projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet
[coq-hetmet.git]
/
src
/
HaskProgrammingLanguage.v
diff --git
a/src/HaskProgrammingLanguage.v
b/src/HaskProgrammingLanguage.v
index
8aba304
..
30a0ae8
100644
(file)
--- a/
src/HaskProgrammingLanguage.v
+++ b/
src/HaskProgrammingLanguage.v
@@
-73,10
+73,10
@@
Section HaskProgrammingLanguage.
apply nd_id.
eapply nd_rule.
set (@org_fc) as ofc.
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.
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.
apply nd_rule.
destruct l.
destruct l0.
@@
-148,23
+148,23
@@
Section HaskProgrammingLanguage.
; cnd_expand_right := fun a b c => SystemFCa_right c a b }.
(*
intros; apply nd_rule. simpl.
; 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.
auto.
intros; apply nd_rule. simpl.
- apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))); auto.
+ apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AAssoc _ _ _))); auto.
intros; apply nd_rule. simpl.
intros; apply nd_rule. simpl.
- apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanL _))); auto.
+ apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (ACanL _))); auto.
intros; apply nd_rule. simpl.
intros; apply nd_rule. simpl.
- apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanR _))); auto.
+ apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (ACanR _))); auto.
intros; apply nd_rule. simpl.
intros; apply nd_rule. simpl.
- apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanL _))); auto.
+ apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AuCanL _))); auto.
intros; apply nd_rule. simpl.
intros; apply nd_rule. simpl.
- apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanR _))); auto.
+ apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AuCanR _))); auto.
*)
admit.
admit.
*)
admit.
admit.