X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProgrammingLanguage.v;h=30a0ae82e12578862d17338cce9d5908f6a299ac;hp=9801168b39defa4237b66296b750f7224975b89a;hb=423b0bd3972c5bcbbd757cb715e13b5b9104a9a6;hpb=94ad996f571e3c9fd622bc56d9b57118a7e5333a

diff --git a/src/HaskProgrammingLanguage.v b/src/HaskProgrammingLanguage.v
index 9801168..30a0ae8 100644
--- a/src/HaskProgrammingLanguage.v
+++ b/src/HaskProgrammingLanguage.v
@@ -27,7 +27,8 @@ Require Import Coherence_ch7_8.
 
 Require Import HaskKinds.
 Require Import HaskCoreTypes.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskStrongTypes.
 Require Import HaskProof.
 Require Import NaturalDeduction.
@@ -72,10 +73,10 @@ Section HaskProgrammingLanguage.
       apply nd_id.
       eapply nd_rule.
       set (@org_fc) as ofc.
-      set (RArrange Γ Δ _ _ _ (RuCanL [l0])) as rule.
-      apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [_])).
+      set (RArrange Γ Δ _ _ _ (AuCanL [l0])) as rule.
+      apply org_fc with (r:=RArrange _ _ _ _ _ (AuCanL [_])).
       auto.
-      eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (RCanL _)) ].
+      eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (ACanL _)) ].
       apply nd_rule.
       destruct l.
       destruct l0.
@@ -147,23 +148,23 @@ Section HaskProgrammingLanguage.
   ; cnd_expand_right := fun a b c => SystemFCa_right c a b }.
     (*
     intros; apply nd_rule. simpl.
-      apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (RCossa _ _ _)))).
+      apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (AuAssoc _ _ _)))).
       auto.
 
     intros; apply nd_rule. simpl.
-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))); auto.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AAssoc _ _ _))); auto.
 
     intros; apply nd_rule. simpl.
-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanL _))); auto.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (ACanL _))); auto.
 
     intros; apply nd_rule. simpl.
-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanR _))); auto.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (ACanR _))); auto.
 
     intros; apply nd_rule. simpl.
-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanL _))); auto.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AuCanL _))); auto.
 
     intros; apply nd_rule. simpl.
-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanR _))); auto.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AuCanR _))); auto.
       *)
       admit.
       admit.