projects
/
coq-hetmet.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
aec3c69
)
add ToLatex instance parameter to HaskStrong
author
Adam Megacz
<megacz@cs.berkeley.edu>
Fri, 25 Mar 2011 18:15:01 +0000
(11:15 -0700)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Fri, 25 Mar 2011 18:15:01 +0000
(11:15 -0700)
src/HaskStrong.v
patch
|
blob
|
history
diff --git
a/src/HaskStrong.v
b/src/HaskStrong.v
index
1f4d03b
..
6539c89
100644
(file)
--- a/
src/HaskStrong.v
+++ b/
src/HaskStrong.v
@@
-12,6
+12,7
@@
Require Import HaskCoreTypes.
Require Import HaskLiteralsAndTyCons.
Require Import HaskStrongTypes.
Require Import HaskWeakVars.
Require Import HaskLiteralsAndTyCons.
Require Import HaskStrongTypes.
Require Import HaskWeakVars.
+Require Import HaskCoreVars.
Section HaskStrong.
Section HaskStrong.
@@
-74,11
+75,8
@@
Section HaskStrong.
| ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2)
.
| ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2)
.
-
Context {ToStringVV:ToString VV}.
Context {ToStringVV:ToString VV}.
-
- Require Import HaskCoreVars.
-
+ Context {ToLatexVV:ToLatex VV}.
Fixpoint exprToString {Γ}{Δ}{ξ}{τ}(exp:Expr Γ Δ ξ τ) : string :=
match exp with
| EVar Γ' _ ξ' ev => "var."+++ev
Fixpoint exprToString {Γ}{Δ}{ξ}{τ}(exp:Expr Γ Δ ξ τ) : string :=
match exp with
| EVar Γ' _ ξ' ev => "var."+++ev