X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToCore.v;fp=src%2FHaskWeakToCore.v;h=b6add9448794403c5c9de6c77baff31dfdd1447c;hp=e4a4d1ff930d1aa41a46010e5692a99d639dc0a2;hb=825fa62636c32762ac2e1c1357209119de74c281;hpb=54e3d85658516dcf7d8504e94f973a87e255f8f3

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