separate type/coer/expr variables in HaskWeak case branches

[coq-hetmet.git] / src / HaskWeakVars.v

diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v
index c43842f..2e242c8 100644 (file)
--- 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.