X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FPCF.v;h=373519b72a1431f4b989a701480c22254fdfc427;hp=5caf2dc01e3676721c44813dc3511fa28a5b60c8;hb=1a2754d2e135ef3c5fd7ef817e1129af93b533a5;hpb=91f06dc68cf5888360f1819429b10e054f94b243;ds=sidebyside

diff --git a/src/PCF.v b/src/PCF.v
index 5caf2dc..373519b 100644
--- a/src/PCF.v
+++ b/src/PCF.v
@@ -183,8 +183,8 @@ Section PCF.
       eapply nd_prod.
       apply nd_id.
       apply (PCF_Arrange [h] ([],,[h]) [h0]).
-      apply RuCanL.
-      eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply RCanL ].
+      apply AuCanL.
+      eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply ACanL ].
       apply nd_rule.
       (*
       set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.
@@ -241,27 +241,27 @@ Section PCF.
   ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }.
 
     intros; apply nd_rule. unfold PCFRule. simpl.
-      exists (RArrange _ _ _ _ _ (RCossa _ _ _)).
+      exists (RArrange _ _ _ _ _ (AuAssoc _ _ _)).
       apply (PCF_RArrange _ _ lev ((a,,b),,c) (a,,(b,,c)) x).
 
     intros; apply nd_rule. unfold PCFRule. simpl.
-      exists (RArrange _ _ _ _ _ (RAssoc _ _ _)).
+      exists (RArrange _ _ _ _ _ (AAssoc _ _ _)).
       apply (PCF_RArrange _ _ lev (a,,(b,,c)) ((a,,b),,c) x).
 
     intros; apply nd_rule. unfold PCFRule. simpl.
-      exists (RArrange _ _ _ _ _ (RCanL _)).
+      exists (RArrange _ _ _ _ _ (ACanL _)).
       apply (PCF_RArrange _ _ lev ([],,a) _ _).
 
     intros; apply nd_rule. unfold PCFRule. simpl.
-      exists (RArrange _ _ _ _ _ (RCanR _)).
+      exists (RArrange _ _ _ _ _ (ACanR _)).
       apply (PCF_RArrange _ _ lev (a,,[]) _ _).
 
     intros; apply nd_rule. unfold PCFRule. simpl.
-      exists (RArrange _ _ _ _ _ (RuCanL _)).
+      exists (RArrange _ _ _ _ _ (AuCanL _)).
       apply (PCF_RArrange _ _ lev _ ([],,a) _).
 
     intros; apply nd_rule. unfold PCFRule. simpl.
-      exists (RArrange _ _ _ _ _ (RuCanR _)).
+      exists (RArrange _ _ _ _ _ (AuCanR _)).
       apply (PCF_RArrange _ _ lev _ (a,,[]) _).
       Defined.