diff options
| author | herbelin | 2006-01-11 09:47:32 +0000 |
|---|---|---|
| committer | herbelin | 2006-01-11 09:47:32 +0000 |
| commit | dcaefd4a668617504aaf335ed346598b03a80ba1 (patch) | |
| tree | 9b97ca322252777d101152452193d0a7c8537e2e /contrib/xml/doubleTypeInference.ml | |
| parent | 88d15de0cc467368dc71851e995d82093f9692ca (diff) | |
Restructuration et simplification des fonctions d'affichage, de détypage
et d'"externalisation"; standardisation du nom des fonctions d'affichage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml/doubleTypeInference.ml')
| -rw-r--r-- | contrib/xml/doubleTypeInference.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index 24676f1866..518f6c115f 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -40,13 +40,13 @@ let whd_betadeltaiotacprop env evar_map ty = Conv_oracle.set_opaque_const cprop; prerr_endline "###whd_betadeltaiotacprop:" ; let xxx = -(*Pp.msgerr (Printer.prterm_env env ty);*) +(*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.prterm_env env xxx); +Pp.msgerr (Printer.pr_lconstr_env env xxx); *) prerr_endline ""; Conv_oracle.set_transparent_const cprop; @@ -258,7 +258,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = in (*CSC: debugging stuff to be removed *) if Acic.CicHash.mem subterms_to_types cstr then - (Pp.ppnl (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.prterm cstr)) ; flush stdout ) ; + (Pp.ppnl (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.pr_lconstr cstr)) ; flush stdout ) ; Acic.CicHash.add subterms_to_types cstr types ; E.make_judge cstr res |