X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskWeakToCore.v;h=b6add9448794403c5c9de6c77baff31dfdd1447c;hb=53d4f1ce851b924cab5dc39419179a366001cbca;hp=e4a4d1ff930d1aa41a46010e5692a99d639dc0a2;hpb=ab2e0681a81695cc2380b007f2a3314005ec1c99;p=coq-hetmet.git

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index e4a4d1f..b6add94 100644
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -31,10 +31,10 @@ Variable mkUnsafeCoercion : CoreType -> CoreType -> CoreCoercion.
 Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
   Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
 
-  Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
-    mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
+Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
+  mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
 
-  Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
+Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
   match me with
   | WEVar   (weakExprVar v _)            => CoreEVar  v
   | WELit   lit                          => CoreELit  lit