-
-Definition weakVarToCoreVar (wv:WeakVar) : CoreVar :=
-match wv with
-| WExprVar (weakExprVar v _ ) => v
-| WTypeVar (weakTypeVar v _ ) => v
-| WCoerVar (weakCoerVar v _ _ ) => v
-end.
-Coercion weakVarToCoreVar : WeakVar >-> CoreVar.
+ (* FIXME this doesn't actually work *)
+ Extract Inlined Constant dummyVariable => "(Prelude.error ""dummyVariable"")".