X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakVars.v;h=2e242c88aa23bbd8a6ca14b200c87b8c4cafde8e;hp=c43842fe02d85716697f8a88e589899a897ae9ab;hb=02af384ece10c5aa927c7d7c1379e9d202926cc8;hpb=94c8e7297c8026cb505bb0a8461da4a0b257b48a

diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v
index c43842f..2e242c8 100644
--- a/src/HaskWeakVars.v
+++ b/src/HaskWeakVars.v
@@ -24,13 +24,18 @@ Inductive WeakVar : Type :=
 | WExprVar : WeakExprVar -> WeakVar
 | WTypeVar : WeakTypeVar -> WeakVar
 | WCoerVar : WeakCoerVar -> WeakVar.
+Coercion WExprVar : WeakExprVar >-> WeakVar.
+Coercion WTypeVar : WeakTypeVar >-> WeakVar.
+Coercion WCoerVar : WeakCoerVar >-> WeakVar.
+
 
 Definition haskLiteralToCoreType lit : CoreType :=
   TyConApp (haskLiteralToTyCon lit) nil.
 
 Definition weakTypeToCoreType (wt:CoreType) : CoreType := wt.
 
-Definition weakTypeToString : CoreType -> string := coreTypeToString ○ weakTypeToCoreType.
+Definition weakTypeToString : CoreType -> string :=
+  coreTypeToString ○ weakTypeToCoreType.
 
 (* EqDecidable instances for all of the above *)
 Instance CoreTypeVarEqDecidable : EqDecidable WeakTypeVar.