X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongTypes.v;h=e5a10ba05665edf76709ca8d816c4a051ac8260c;hp=24f349bf7e30cff7a66bdb48100bccc538f18a7f;hb=5cb97fa6ed28f55ca888bdadc4f145396cc02236;hpb=57e387249da84dac0f1c5a9411e3900831ce2d81

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index 24f349b..e5a10ba 100644
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -19,11 +19,11 @@ Require Import HaskCoreToWeak.
 
 Variable dataConTyCon      : CoreDataCon -> TyCon.         Extract Inlined Constant dataConTyCon      => "DataCon.dataConTyCon".
 Variable dataConExVars_    : CoreDataCon -> list CoreVar.  Extract Inlined Constant dataConExVars_    => "DataCon.dataConExTyVars".
-Variable dataConEqTheta_   : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_   => "DataCon.dataConEqTheta".
+Variable dataConEqTheta_   : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_   => "DataCon.dataConTheta".
 Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys".
 
 Definition dataConExTyVars cdc :=
-  filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)).
+  filter (map (fun x => match coreVarToWeakVar' x with OK (WTypeVar v) => Some v | _ => None end) (dataConExVars_ cdc)).
   Opaque dataConExTyVars.
 Definition dataConCoerKinds cdc :=
   filter (map (fun x => match x with EqPred t1 t2 =>