X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=c1e54aa9499a323352376f3c7753d1deb97532ba;hb=64d416692bda1d36c33b5efa245d46dcf546ad4a;hp=d5e57f89f75acdacb040d18e8b19d063afb2b166;hpb=ec8ee5cde986e5b38bcae38cda9e63eba94f1d9f;p=coq-hetmet.git

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index d5e57f8..c1e54aa 100644
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -581,12 +581,12 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
       |- (mapOptionTree (@snd _ _) tree) @@@ lev ].
   intro X; induction X; intros; simpl in *.
     apply nd_rule.
-      apply REmptyGroup.
+      apply RVoid.
     set (ξ v) as q in *.
       destruct q.
       simpl in *.
       apply n.
-    eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
+    eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
     eapply nd_comp; [ apply nd_llecnac | idtac ].
     apply nd_prod; auto.
   Defined.
@@ -639,7 +639,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
   simpl.
 
   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
-    eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
+    eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
     eapply nd_comp; [ apply nd_llecnac | idtac ].
     apply nd_prod; auto.
     rewrite ξlemma.