projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
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 General.
Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
Require Import HaskKinds.
Require Import HaskLiterals.
Require Import HaskKinds.
Require Import HaskLiterals.
@@
-236,7
+237,7
@@
Section core2proof.
ND Rule
[ Γ > Δ > Σ |- [a ---> s ]@lev ]
[ Γ > Δ > [a @@ lev],,Σ |- [ s ]@lev ].
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.
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.
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.
apply curry.
Defined.
@@
-267,8
+268,8
@@
Section core2proof.
eapply nd_comp.
eapply nd_rule.
eapply RArrange.
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.
apply curry.
Defined.