diff options
Diffstat (limited to 'contrib/xml/doubleTypeInference.ml')
-rw-r--r-- | contrib/xml/doubleTypeInference.ml | 30 |
1 files changed, 6 insertions, 24 deletions
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index c7d3b4ff..cce78891 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -26,31 +26,13 @@ let cprop = (N.mk_label "CProp") ;; -let whd_betadeltaiotacprop env evar_map ty = +let whd_betadeltaiotacprop env _evar_map ty = let module R = Rawterm in - let red_exp = - R.Hnf (*** Instead CProp is made Opaque ***) -(* - R.Cbv - {R.rBeta = true ; R.rIota = true ; R.rDelta = true; R.rZeta=true ; - R.rConst = [Names.EvalConstRef cprop] - } -*) - in -Conv_oracle.set_opaque_const cprop; -prerr_endline "###whd_betadeltaiotacprop:" ; -let xxx = -(*Pp.msgerr (Printer.pr_lconstr_env env ty);*) -prerr_endline ""; - (fst (Redexpr.reduction_of_red_expr red_exp)) env evar_map ty -in -prerr_endline "###FINE" ; -(* -Pp.msgerr (Printer.pr_lconstr_env env xxx); -*) -prerr_endline ""; -Conv_oracle.set_transparent_const cprop; -xxx + let module C = Closure in + let module CR = C.RedFlags in + (*** CProp is made Opaque ***) + let flags = CR.red_sub C.betadeltaiota (CR.fCONST cprop) in + C.whd_val (C.create_clos_infos flags env) (C.inject ty) ;; |