X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtractionMain.v;h=df7896b14e5330fecfecbe1c88e5c09a2db56f9e;hp=77326e0054370762fbe7dc90a8d4a1130ff8154d;hb=1a2754d2e135ef3c5fd7ef817e1129af93b533a5;hpb=57e387249da84dac0f1c5a9411e3900831ce2d81

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 77326e0..df7896b 100644
--- 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.
@@ -132,7 +133,7 @@ Section core2proof.
                     OK (eol+++eol+++eol+++
                         "\begin{preview}"+++eol+++
                         "$\displaystyle "+++
-                        toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++
+                        toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ _ e))+++
                         " $"+++eol+++
                         "\end{preview}"+++eol+++eol+++eol)
                   )))))))).
@@ -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.
 
@@ -432,9 +433,9 @@ Section core2proof.
 
                       (addErrorMessage ("HaskStrong...")
                         (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten'
-                                            hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ e)
+                                            hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ _ e)
                          in (* insert HaskProof-to-HaskProof manipulations here *)
-                         OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ@@nil) _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
+                         OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
                          >>= fun e' =>
                            (snd e') >>= fun e'' =>
                          strongExprToWeakExpr hetmet_brak' hetmet_esc'