X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskLiteralsAndTyCons.v;h=62d638bbdcf753588d513ed02c1828985156ecdb;hp=1b8494f3badf03a8e38d4c9b49dd1124e163f6f7;hb=ec8ee5cde986e5b38bcae38cda9e63eba94f1d9f;hpb=b096aab78240e38ff69c120367e65be60cbc54f5

diff --git a/src/HaskLiteralsAndTyCons.v b/src/HaskLiteralsAndTyCons.v
index 1b8494f..62d638b 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 :=