rename constructors of Arrange to start with A instead of R

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

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 4da66c7..df7896b 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -13,6 +13,7 @@ Require Import Preamble.
 Require Import General.
 
 Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
 
 Require Import HaskKinds.
 Require Import HaskLiterals.
@@ -236,7 +237,7 @@ Section core2proof.
     ND Rule 
        [ Γ > Δ > Σ             |- [a ---> s  ]@lev ]
        [ Γ > Δ > [a @@ lev],,Σ |-       [ s ]@lev ].
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
@@ -251,7 +252,7 @@ Section core2proof.
     intro pf.
     eapply nd_comp.
     apply pf.
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ].
     apply curry.
     Defined.
 
@@ -267,8 +268,8 @@ Section core2proof.
     eapply nd_comp.
     eapply nd_rule.
     eapply RArrange.
-    eapply RCanR.
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+    eapply ACanR.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
     apply curry.
     Defined.