X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongTypes.v;h=e5a10ba05665edf76709ca8d816c4a051ac8260c;hp=60e84b67eaa9b2e53c7bfc76e9e86c3695bc3089;hb=0f137f4fbe7076b7a0f6b33d661b4f7aa8b4f160;hpb=d97b00a6ff6e8e2244927d17bda4b9762fc3d716 diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 60e84b6..e5a10ba 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -19,7 +19,7 @@ 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 :=