remove RJoin rule

[coq-hetmet.git] / src / HaskProofToStrong.v

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index b16d4a8..2ea0c4a 100644 (file)
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -768,7 +768,6 @@ Section HaskProofToStrong.
       | RLeft   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
       | RRight  Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
       | RWhere  Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p  => let case_RWhere := tt          in _
       | RLeft   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
       | RRight  Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
       | RWhere  Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p  => let case_RWhere := tt          in _

-      | RJoin   Γ p lri m x q l       => let case_RJoin := tt in _

       | RVoid   _ _ l                 => let case_RVoid := tt   in _
       | RBrak   Σ a b c n m           => let case_RBrak := tt         in _
       | REsc    Σ a b c n m           => let case_REsc := tt          in _
       | RVoid   _ _ l                 => let case_RVoid := tt   in _
       | RBrak   Σ a b c n m           => let case_RBrak := tt         in _
       | REsc    Σ a b c n m           => let case_REsc := tt          in _

@@ -849,19 +848,6 @@ Section HaskProofToStrong.
     apply ileaf in X. simpl in X.
     apply X.
 
     apply ileaf in X. simpl in X.
     apply X.
 

-  destruct case_RJoin.
-    apply ILeaf; simpl; intros.
-    inversion X_.
-    apply ileaf in X.
-    apply ileaf in X0.
-    simpl in *.
-    destruct vars; inversion H.
-    destruct o; inversion H3.
-    refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
-    apply FreshMon.
-    apply FreshMon.
-    apply IBranch; auto.
-

   destruct case_RApp.    
     apply ILeaf.
     inversion X_.
   destruct case_RApp.    
     apply ILeaf.
     inversion X_.