X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskLiteralsAndTyCons.v;h=1b8494f3badf03a8e38d4c9b49dd1124e163f6f7;hp=a0695d227990c35586fff15c159a40d6ed20f83a;hb=97552c1a6dfb32098d4491951929ab1d4aca96a0;hpb=92e148ed7a7b0068cf2029537b019a88a7b07d43 diff --git a/src/HaskLiteralsAndTyCons.v b/src/HaskLiteralsAndTyCons.v index a0695d2..1b8494f 100644 --- a/src/HaskLiteralsAndTyCons.v +++ b/src/HaskLiteralsAndTyCons.v @@ -86,8 +86,8 @@ Variable tyConToString : TyCon -> string. Extract Inlined Constant tyCon Variable tyFunToString : TyFun -> string. Extract Inlined Constant tyFunToString => "outputableToString". Instance TyConToString : ToString TyCon := { toString := tyConToString }. Instance TyFunToString : ToString TyFun := { toString := tyFunToString }. -Instance TyConToLatex : ToLatex TyCon := { toLatex := fun x => latex (sanitizeForLatex (toString x)) }. -Instance TyFunToLatex : ToLatex TyCon := { toLatex := fun x => latex (sanitizeForLatex (toString x)) }. +Instance TyConToLatex : ToLatex TyCon := { toLatex := fun x => toLatex (toString x) }. +Instance TyFunToLatex : ToLatex TyCon := { toLatex := fun x => toLatex (toString x) }. Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon". Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon".