Correction de plusieurs bugs de l'export XML (utilisation d'un type de

constante par defaut pour les nouveaux types plutot qu'echouer;
avertissement plutot qu'echec en cas de foncteur; nommage systematique
des LetIn -- p.ex. functional induction engendre des LetIn non nommes --;
branchement de la fonction de normalisation de tete evitant CProp
sur Closure au lieu de Tacred afin de garantir la f.n. de tete)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9902 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 24 deletions

diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index c7d3b4ff0c..cce788912d 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)
 ;;