X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskLiteralsAndTyCons.v;h=a0695d227990c35586fff15c159a40d6ed20f83a;hp=0592f3abbdc1beb8dd823f467c56ace10dbcde4a;hb=92e148ed7a7b0068cf2029537b019a88a7b07d43;hpb=68f1cdc7daa1e2d9ba9ff343ccf7ec51082a2255

diff --git a/src/HaskLiteralsAndTyCons.v b/src/HaskLiteralsAndTyCons.v
index 0592f3a..a0695d2 100644
--- a/src/HaskLiteralsAndTyCons.v
+++ b/src/HaskLiteralsAndTyCons.v
@@ -86,6 +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)) }.
 
 Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
 Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".