add ToLatex instance for TyCon/TyFun

diff --git a/src/HaskLiteralsAndTyCons.v b/src/HaskLiteralsAndTyCons.v
index 0592f3a..a0695d2 100644 (file)
--- 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".

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index fab70fe..d99469c 100644 (file)
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -27,10 +27,6 @@ Section HaskProofToLatex.
   Definition FreshM' := FMT freshM.
   Instance FreshMon' : Monad FreshM' := FMT_Monad freshM.
   
-  Instance ToLatexTyCon : ToLatex TyCon.
-    admit.
-    Defined.
-
   Fixpoint typeToLatex (needparens:bool){κ}(t:RawHaskType TV κ) {struct t} : FMT freshM Latex :=
     match t with
     | TVar    _ v        => return toLatex v