X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToStrong.v;h=b6e8efee00b3730606325935a866162a67bb9ffa;hp=52f2154baa02382b6a3fe9394e9c657088e4bb0a;hb=93ac0d63048027161f816c451a7954fb8a6470c0;hpb=9e7ea73d3a6f4bbfba279164a806490cf95efec4

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 52f2154..b6e8efe 100644
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -239,6 +239,7 @@ Section HaskProofToStrong.
  with
           | RLeft   h c ctx r => let case_RLeft  := tt in (fun e => _) (urule2expr _ _ _ r)
           | RRight  h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ r)
+          | RId     a       => let case_RId    := tt in _
           | RCanL   a       => let case_RCanL  := tt in _
           | RCanR   a       => let case_RCanR  := tt in _
           | RuCanL  a       => let case_RuCanL := tt in _
@@ -251,6 +252,9 @@ Section HaskProofToStrong.
           | RComp   a b c f g => let case_RComp  := tt in (fun e1 e2 => _) (urule2expr _ _ _ f) (urule2expr _ _ _ g)
           end); clear urule2expr; intros.
 
+      destruct case_RId.
+        apply X.
+
       destruct case_RCanL.
         simpl; unfold ujudg2exprType; intros.
         simpl in X.
@@ -569,7 +573,6 @@ Section HaskProofToStrong.
   destruct case_RGlobal.
     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
     apply EGlobal.
-    apply wev.
 
   destruct case_RLam.
     apply ILeaf.
@@ -633,7 +636,7 @@ Section HaskProofToStrong.
     apply ileaf in q1'.
     apply ileaf in q2'.
     simpl in *.
-    apply (EApp _ _ _ _ _ _ q1' q2').
+    apply (EApp _ _ _ _ _ _ q2' q1').
 
   destruct case_RLet.
     apply ILeaf.
@@ -715,6 +718,7 @@ Section HaskProofToStrong.
     inversion X; subst; clear X.
 
     apply (@ELetRec _ _ _ _ _ _ _ varstypes).
+    auto.
     apply (@letrec_helper Γ Δ t varstypes).
     rewrite <- pf2 in X1.
     rewrite mapOptionTree_compose.