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

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index fab70fe..d99469c 100644
--- 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