From: Adam Megacz Date: Fri, 25 Mar 2011 18:15:01 +0000 (-0700) Subject: add ToLatex instance parameter to HaskStrong X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=fba815a8a6107b5cdf3a99bd77df34d4b05e702c add ToLatex instance parameter to HaskStrong --- diff --git a/src/HaskStrong.v b/src/HaskStrong.v index 1f4d03b..6539c89 100644 --- 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 HaskCoreVars. Section HaskStrong. @@ -74,11 +75,8 @@ Section HaskStrong. | ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2) . - Context {ToStringVV:ToString VV}. - - Require Import HaskCoreVars. - + Context {ToLatexVV:ToLatex VV}. Fixpoint exprToString {Γ}{Δ}{ξ}{τ}(exp:Expr Γ Δ ξ τ) : string := match exp with | EVar Γ' _ ξ' ev => "var."+++ev