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

diff --git a/src/HaskLiteralsAndTyCons.v b/src/HaskLiteralsAndTyCons.v
index a0695d2..38e7f95 100644
--- a/src/HaskLiteralsAndTyCons.v
+++ b/src/HaskLiteralsAndTyCons.v
@@ -15,16 +15,16 @@ Variable TyCon           : Type.                      Extract Inlined Constant T
 Variable TyFun           : Type.                      Extract Inlined Constant TyFun                => "TyCon.TyCon".
 
 (* Since GHC is written in Haskell, compile-time Haskell constants are represented using Haskell (Prelude) types *)
-Variable HaskInt                 : Type.      Extract Inlined Constant HaskInt             => "Prelude.Int".
-Variable HaskChar                : Type.      Extract Inlined Constant HaskChar            => "Prelude.Char".
-Variable HaskFastString          : Type.      Extract Inlined Constant HaskFastString      => "FastString.FastString".
-Variable HaskInteger             : Type.      Extract Inlined Constant HaskInteger         => "Prelude.Integer".
-Variable HaskRational            : Type.      Extract Inlined Constant HaskRational        => "Prelude.Rational".
+Variable HaskInt         : Type.                      Extract Inlined Constant HaskInt               => "Prelude.Int".
+Variable HaskChar        : Type.                      Extract Inlined Constant HaskChar              => "Prelude.Char".
+Variable HaskFastString  : Type.                      Extract Inlined Constant HaskFastString        => "FastString.FastString".
+Variable HaskInteger     : Type.                      Extract Inlined Constant HaskInteger           => "Prelude.Integer".
+Variable HaskRational    : Type.                      Extract Inlined Constant HaskRational          => "Prelude.Rational".
 
-Variable CoreName            : Type.                      Extract Inlined Constant CoreName              => "Name.Name".
-Variable Class_              : Type.                      Extract Inlined Constant Class_                => "Class.Class".
-Variable CoreIPName          : Type -> Type.              Extract         Constant CoreIPName "’a"       => "BasicTypes.IPName".
-                                                          Extraction Inline CoreIPName.
+Variable CoreName        : Type.                      Extract Inlined Constant CoreName              => "Name.Name".
+Variable Class_          : Type.                      Extract Inlined Constant Class_                => "Class.Class".
+Variable CoreIPName      : Type -> Type.              Extract         Constant CoreIPName "’a"       => "BasicTypes.IPName".
+                                                      Extraction Inline CoreIPName.
 
 (* This type extracts exactly onto GHC's Literal.Literal type *)
 Inductive HaskLiteral :=
@@ -86,8 +86,10 @@ 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 PairTyCon       : TyFun.        Extract Inlined Constant PairTyCon     => "TysWiredIn.pairTyCon".
+Variable UnitTyCon       : TyFun.        Extract Inlined Constant UnitTyCon     => "TysWiredIn.unitTyCon".
 Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".