aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/correctness/ptactic.ml8
-rw-r--r--contrib/correctness/putil.ml14
-rw-r--r--contrib/dp/dp.ml2
-rw-r--r--contrib/field/field.ml42
-rw-r--r--contrib/first-order/instances.ml2
-rw-r--r--contrib/first-order/sequent.ml2
-rw-r--r--contrib/funind/tacinvutils.ml6
-rw-r--r--contrib/interface/centaur.ml46
-rw-r--r--contrib/interface/showproof_ct.ml2
-rw-r--r--contrib/interface/translate.mli2
-rw-r--r--contrib/jprover/jprover.ml42
-rw-r--r--contrib/omega/coq_omega.ml6
-rw-r--r--contrib/ring/ring.ml4
-rw-r--r--contrib/romega/refl_omega.ml2
-rw-r--r--contrib/setoid_ring/newring.ml419
-rw-r--r--contrib/subtac/infer.ml8
-rw-r--r--contrib/subtac/rewrite.ml10
-rw-r--r--contrib/xml/cic2acic.ml6
-rw-r--r--contrib/xml/doubleTypeInference.ml6
-rw-r--r--contrib/xml/proofTree2Xml.ml46
20 files changed, 58 insertions, 57 deletions
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index bd742b9dfc..5994fb38d4 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -51,7 +51,7 @@ let coqast_of_prog p =
(* 4a. traduction type *)
let ty = Pmonad.trad_ml_type_c ren env c in
- deb_print (Printer.prterm_env (Global.env())) ty;
+ deb_print (Printer.pr_lconstr_env (Global.env())) ty;
(* 4b. traduction terme (terme intermédiaire de type cc_term) *)
deb_mess
@@ -65,12 +65,12 @@ let coqast_of_prog p =
(fnl () ++ str"Pcic.constr_of_prog: Translation cc_term -> rawconstr..." ++
fnl ());
let r = Pcic.rawconstr_of_prog cc in
- deb_print Printer.pr_rawterm r;
+ deb_print Printer.pr_lrawconstr r;
(* 6. résolution implicites *)
deb_mess (fnl () ++ str"Resolution implicits (? => Meta(n))..." ++ fnl ());
let oc = understand_gen_tcc Evd.empty (Global.env()) [] None r in
- deb_print (Printer.prterm_env (Global.env())) (snd oc);
+ deb_print (Printer.pr_lconstr_env (Global.env())) (snd oc);
p,oc,ty,v
@@ -248,7 +248,7 @@ let correctness s p opttac =
deb_mess (str"Pred.red_cci: Reduction..." ++ fnl ());
let oc = reduce_open_constr oc in
deb_mess (str"AFTER REDUCTION:" ++ fnl ());
- deb_print (Printer.prterm_env (Global.env())) (snd oc);
+ deb_print (Printer.pr_lconstr_env (Global.env())) (snd oc);
let tac = (tclTHEN (Extratactics.refine_tac oc) automatic) in
let tac = match opttac with
| None -> tac
diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml
index 45fdb75ec7..29064578f1 100644
--- a/contrib/correctness/putil.ml
+++ b/contrib/correctness/putil.ml
@@ -231,26 +231,26 @@ and c_of_constr c =
open Pp
open Util
-let prterm x = Printer.prterm_env (Global.env()) x
+let pr_lconstr x = Printer.pr_lconstr_env (Global.env()) x
let pp_pre = function
[] -> (mt ())
| l ->
hov 0 (str"pre " ++
prlist_with_sep (fun () -> (spc ()))
- (fun x -> prterm x.p_value) l)
+ (fun x -> pr_lconstr x.p_value) l)
let pp_post = function
None -> (mt ())
- | Some c -> hov 0 (str"post " ++ prterm c.a_value)
+ | Some c -> hov 0 (str"post " ++ pr_lconstr c.a_value)
let rec pp_type_v = function
Ref v -> hov 0 (pp_type_v v ++ spc () ++ str"ref")
- | Array (cc,v) -> hov 0 (str"array " ++ prterm cc ++ str" of " ++ pp_type_v v)
+ | Array (cc,v) -> hov 0 (str"array " ++ pr_lconstr cc ++ str" of " ++ pp_type_v v)
| Arrow (b,c) ->
hov 0 (prlist_with_sep (fun () -> (mt ())) pp_binder b ++
pp_type_c c)
- | TypePure c -> prterm c
+ | TypePure c -> pr_lconstr c
and pp_type_c ((id,v),e,p,q) =
hov 0 (str"returns " ++ pr_id id ++ str":" ++ pp_type_v v ++ spc () ++
@@ -297,7 +297,7 @@ let rec pp_cc_term = function
| CC_case _ ->
hov 0 (str"<Case: not yet implemented>")
| CC_expr c ->
- hov 0 (prterm c)
+ hov 0 (pr_lconstr c)
| CC_hole c ->
- (str"(?::" ++ prterm c ++ str")")
+ (str"(?::" ++ pr_lconstr c ++ str")")
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index f25794e804..32b39b03d2 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -172,7 +172,7 @@ let rec_names_for c =
| Name id ->
let c' = Names.make_con mp dp (label_of_id id) in
ignore (Global.lookup_constant c');
- msgnl (Ppconstr.pr_term (mkConst c'));
+ msgnl (Printer.pr_constr (mkConst c'));
c'
| Anonymous ->
raise Not_found)
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index f0a5489df0..90a9863857 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -44,7 +44,7 @@ let lookup env typ =
with Not_found ->
errorlabstrm "field"
(str "No field is declared for type" ++ spc() ++
- Printer.prterm_env env typ)
+ Printer.pr_lconstr_env env typ)
let _ =
let init () = th_tab := Gmap.empty in
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index 7dc01a461e..0b371966b9 100644
--- a/contrib/first-order/instances.ml
+++ b/contrib/first-order/instances.ml
@@ -121,7 +121,7 @@ let mk_open_instance id gl m t=
let nid=(fresh_id avoid var_id gl) in
(Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
let nt=it_mkLambda_or_LetIn revt (aux m []) in
- let rawt=Detyping.detype (false,env) [] [] nt in
+ let rawt=Detyping.detype false [] [] nt in
let rec raux n t=
if n=0 then t else
match t with
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index f9ebafc2a0..c1175a4d9c 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -291,7 +291,7 @@ let print_cmap map=
str "| " ++
Util.prlist Printer.pr_global l ++
str " : " ++
- Ppconstr.pr_constr xc ++
+ Ppconstr.pr_constr_expr xc ++
cut () ++
s in
msgnl (v 0
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index 064f279f0e..2877c19db9 100644
--- a/contrib/funind/tacinvutils.ml
+++ b/contrib/funind/tacinvutils.ml
@@ -21,9 +21,9 @@ open Reductionops
(*s printing of constr -- debugging *)
(* comment this line to see debug msgs *)
-let msg x = () ;; let prterm c = str ""
+let msg x = () ;; let pr_lconstr c = str ""
(* uncomment this to see debugging *)
-let prconstr c = msg (str" " ++ prterm c ++ str"\n")
+let prconstr c = msg (str" " ++ pr_lconstr c ++ str"\n")
let prlistconstr lc = List.iter prconstr lc
let prstr s = msg(str s)
@@ -31,7 +31,7 @@ let prchr () = msg (str" (ret) \n")
let prNamedConstr s c =
begin
msg(str "");
- msg(str(s^"==>\n ") ++ prterm c ++ str "\n<==\n");
+ msg(str(s^"==>\n ") ++ pr_lconstr c ++ str "\n<==\n");
msg(str "");
end
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index e79d14249d..81e175232f 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -280,12 +280,12 @@ let print_check judg =
let value_ct_ast =
(try translate_constr false (Global.env()) value
with UserError(f,str) ->
- raise(UserError(f,Printer.prterm value ++
+ raise(UserError(f,Printer.pr_lconstr value ++
fnl () ++ str ))) in
let type_ct_ast =
(try translate_constr false (Global.env()) typ
with UserError(f,str) ->
- raise(UserError(f, Printer.prterm value ++ fnl() ++ str))) in
+ raise(UserError(f, Printer.pr_lconstr value ++ fnl() ++ str))) in
((ctf_SearchResults !global_request_id),
(Some (P_pl
(CT_premises_list
@@ -557,7 +557,7 @@ let rec hyp_pattern_filter pat name a c =
match kind_of_term c with
| Prod(_, hyp, c2) ->
(try
-(* let _ = msgnl ((str "WHOLE ") ++ (Printer.prterm c)) in
+(* let _ = msgnl ((str "WHOLE ") ++ (Printer.pr_lconstr c)) in
let _ = msgnl ((str "PAT ") ++ (Printer.pr_pattern pat)) in *)
if Matching.is_matching pat hyp then
(msgnl (str "ok"); true)
diff --git a/contrib/interface/showproof_ct.ml b/contrib/interface/showproof_ct.ml
index f6ab47376b..07ac73b6aa 100644
--- a/contrib/interface/showproof_ct.ml
+++ b/contrib/interface/showproof_ct.ml
@@ -130,7 +130,7 @@ let rec sp_print x =
| "\n" -> fnl ()
| "Retour chariot pour Show proof" -> fnl ()
|_ -> str s)
- | CT_text_formula f -> prterm (Hashtbl.find ct_FORMULA_constr f)
+ | CT_text_formula f -> pr_lconstr (Hashtbl.find ct_FORMULA_constr f)
| CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "to_prove");
CT_text_path (CT_signed_int_list p);
CT_coerce_ID_to_TEXT (CT_ident "goal");
diff --git a/contrib/interface/translate.mli b/contrib/interface/translate.mli
index 65d8331b2d..9f25ce38a4 100644
--- a/contrib/interface/translate.mli
+++ b/contrib/interface/translate.mli
@@ -6,6 +6,6 @@ open Term;;
val translate_goal : goal -> ct_RULE;;
(* The boolean argument indicates whether names from the environment should *)
-(* be avoided (same interpretation as for prterm_env and ast_of_constr) *)
+(* be avoided (same interpretation as for pr_lconstr_env and ast_of_constr) *)
val translate_constr : bool -> env -> constr -> ct_FORMULA;;
val translate_path : int list -> ct_SIGNED_INT_LIST;;
diff --git a/contrib/jprover/jprover.ml4 b/contrib/jprover/jprover.ml4
index 467036e08e..294943f7df 100644
--- a/contrib/jprover/jprover.ml4
+++ b/contrib/jprover/jprover.ml4
@@ -51,7 +51,7 @@ let mbreak s = Format.print_flush (); print_string ("-break at: "^s);
let jp_error re = raise (JT.RefineError ("jprover", JT.StringError re))
(* print Coq constructor *)
-let print_constr ct = Pp.ppnl (PR.prterm ct); Format.print_flush ()
+let print_constr ct = Pp.ppnl (PR.pr_lconstr ct); Format.print_flush ()
let rec print_constr_list = function
| [] -> ()
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 5d43b1686e..8387b7f63b 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -490,7 +490,7 @@ let context operation path (t : constr) =
| ((P_TYPE :: p), LetIn (n,b,t,c)) ->
(mkLetIn (n,b,loop i p t,c))
| (p, _) ->
- ppnl (Printer.prterm t);
+ ppnl (Printer.pr_lconstr t);
failwith ("abstract_path " ^ string_of_int(List.length p))
in
loop 1 path t
@@ -511,7 +511,7 @@ let occurence path (t : constr) =
| ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term
| ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term
| (p, _) ->
- ppnl (Printer.prterm t);
+ ppnl (Printer.pr_lconstr t);
failwith ("occurence " ^ string_of_int(List.length p))
in
loop path t
@@ -1564,7 +1564,7 @@ let rec decidability gl t =
| Kapp(Nat,[]) -> mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |])
| _ -> errorlabstrm "decidability"
(str "Omega: Can't solve a goal with equality on " ++
- Printer.prterm typ)
+ Printer.pr_lconstr typ)
end
| Kapp(Zne,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zne, [| t1;t2 |])
| Kapp(Zle,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zle, [| t1;t2 |])
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 5448d1389c..48e8763d58 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -287,7 +287,7 @@ let guess_theory a =
with Not_found ->
errorlabstrm "Ring"
(str "No Declared Ring Theory for " ++
- prterm a ++ fnl () ++
+ pr_lconstr a ++ fnl () ++
str "Use Add [Semi] Ring to declare it")
(* Looks up an option *)
@@ -325,7 +325,7 @@ let states_compatibility_for env plus mult opp morphs =
let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus amult aone azero aopp aeq t cset =
if theories_map_mem a then errorlabstrm "Add Semi Ring"
(str "A (Semi-)(Setoid-)Ring Structure is already declared for " ++
- prterm a);
+ pr_lconstr a);
let env = Global.env () in
if (want_ring & want_setoid & (
not (implement_theory env t coq_Setoid_Ring_Theory
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
index 5a7e8afd58..c552da6212 100644
--- a/contrib/romega/refl_omega.ml
+++ b/contrib/romega/refl_omega.ml
@@ -219,7 +219,7 @@ let print_env_reification env =
[] -> Printf.printf " ===============================\n\n"
| t :: l ->
Printf.printf " (%c%02d) := " c i;
- Pp.ppnl (Printer.prterm t);
+ Pp.ppnl (Printer.pr_lconstr t);
Pp.flush_all ();
loop c (succ i) l in
print_newline ();
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 2facb0dcb4..0b0362a3b0 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -31,6 +31,7 @@ open Ppconstr
open Mod_subst
open Tacinterp
open Libobject
+open Printer
(****************************************************************************)
(* Library linking *)
@@ -346,18 +347,18 @@ let default_ring_equality is_semi (r,add,mul,opp,req) =
let op_morph =
op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in
msgnl
- (str"Using setoid \""++pr_term rel.rel_aeq++str"\""++spc()++
- str"and morphisms \""++pr_term add_m.morphism_theory++
- str"\","++spc()++ str"\""++pr_term mul_m.morphism_theory++
- str"\""++spc()++str"and \""++pr_term opp_m.morphism_theory++
+ (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++
+ str"and morphisms \""++pr_constr add_m.morphism_theory++
+ str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++
+ str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++
str"\"");
op_morph)
else
(msgnl
- (str"Using setoid \""++pr_term rel.rel_aeq++str"\"" ++ spc() ++
- str"and morphisms \""++pr_term add_m.morphism_theory++
+ (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++
+ str"and morphisms \""++pr_constr add_m.morphism_theory++
str"\""++spc()++str"and \""++
- pr_term mul_m.morphism_theory++str"\"");
+ pr_constr mul_m.morphism_theory++str"\"");
op_smorph r add mul req add_m.lem mul_m.lem) in
(setoid,op_morph)
@@ -484,7 +485,7 @@ let ring gl =
with Not_found ->
errorlabstrm "ring"
(str"cannot find a declared ring structure for equality"++
- spc()++str"\""++pr_term req++str"\"") in
+ spc()++str"\""++pr_constr req++str"\"") in
let req = carg e.ring_req in
let lemma1 = carg e.ring_lemma1 in
let lemma2 = carg e.ring_lemma2 in
@@ -503,7 +504,7 @@ let ring_rewrite rl =
with Not_found ->
errorlabstrm "ring"
(str"cannot find a declared ring structure over"++
- spc()++str"\""++pr_term ty++str"\"") in
+ spc()++str"\""++pr_constr ty++str"\"") in
let rl = List.fold_right (fun x l -> lapp coq_cons [|ty;x;l|]) rl
(lapp coq_nil [|ty|]) in
Tacinterp.eval_tactic
diff --git a/contrib/subtac/infer.ml b/contrib/subtac/infer.ml
index 987fbedda6..d52d8edf5e 100644
--- a/contrib/subtac/infer.ml
+++ b/contrib/subtac/infer.ml
@@ -6,7 +6,7 @@ open Util
open Sast
open Scoq
open Pp
-open Ppconstr
+open Printer
let ($) f g = fun x -> f (g x)
@@ -385,7 +385,7 @@ let rec print_dterm' ctx = function
++ print_dterm_loc ctx t ++ str ","
++ print_dterm_loc ctx' t' ++ str ":"
++ print_dtype_loc ctx' tt' ++ str ")"
- | DCoq (cstr, t) -> pr_term cstr
+ | DCoq (cstr, t) -> pr_constr cstr
and print_dterm_loc ctx (_, x) = print_dterm' ctx x
(*debug_msg 1 (str ":" ++ print_dtype_loc ctx (type_of_dterm ctx x))*)
@@ -408,10 +408,10 @@ and print_dtype' ctx = function
| DTTerm (t, tt, s) -> str "Term:(" ++ print_dterm_loc ctx t ++ str ")"
| DTInd (n, t, i, s) -> str (string_of_id (snd n))
| DTCoq (c, t, s) ->
- debug_msg 1 (str "Coq:(") ++ pr_term c ++
+ debug_msg 1 (str "Coq:(") ++ pr_constr c ++
debug_msg 1 (str ":" ++ print_dtype_loc ctx t ++ str ")")
| DTSort s ->
- pr_term (mkSort (snd s))
+ pr_constr (mkSort (snd s))
and print_dtype_loc ctx (_, t) = print_dtype' ctx t
diff --git a/contrib/subtac/rewrite.ml b/contrib/subtac/rewrite.ml
index b228be2a70..201f2d48b9 100644
--- a/contrib/subtac/rewrite.ml
+++ b/contrib/subtac/rewrite.ml
@@ -7,7 +7,7 @@ open Term
open Names
open Scoq
open Pp
-open Ppconstr
+open Printer
open Util
type recursion_info = {
@@ -614,7 +614,7 @@ let subtac recursive id (s, t) =
coqt, coqt', coqt', prog_info, [], []
in
trace (str "Rewrite of coqtype done" ++
- str "coqtype' = " ++ pr_term coqtype');
+ str "coqtype' = " ++ pr_constr coqtype');
let dterm, dtype = infer ctx t in
trace (str "Inference done" ++ spc () ++
str "Infered term: " ++ print_dterm_loc ctx dterm ++ spc () ++
@@ -624,9 +624,9 @@ let subtac recursive id (s, t) =
fst (rewrite_type prog_info coqctx dtype)
in
trace (str "Rewrite done" ++ spc () ++
- str "Inferred Coq term:" ++ pr_term dterm' ++ spc () ++
- str "Inferred Coq type:" ++ pr_term dtype' ++ spc () ++
- str "Rewritten Coq type:" ++ pr_term coqtype');
+ str "Inferred Coq term:" ++ pr_constr dterm' ++ spc () ++
+ str "Inferred Coq type:" ++ pr_constr dtype' ++ spc () ++
+ str "Rewritten Coq type:" ++ pr_constr coqtype');
let coercespec = coerce prog_info coqctx dtype' coqtype' in
trace (str "Specs coercion successfull");
let realt = app_opt coercespec dterm' in
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index caac703108..bac7ad7c64 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -388,7 +388,7 @@ try
Acic.CicHash.find terms_to_types tt
with _ ->
(*CSC: Warning: it really happens, for example in Ring_theory!!! *)
-Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.prterm tt)) ; assert false
+Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.pr_lconstr tt)) ; assert false
else
(* We are already in an inner-type and Coscoy's double *)
(* type inference algorithm has not been applied. *)
@@ -402,9 +402,9 @@ Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-ty
in
(* Debugging only:
print_endline "TERMINE:" ; flush stdout ;
-Pp.ppnl (Printer.prterm tt) ; flush stdout ;
+Pp.ppnl (Printer.pr_lconstr tt) ; flush stdout ;
print_endline "TIPO:" ; flush stdout ;
-Pp.ppnl (Printer.prterm synthesized) ; flush stdout ;
+Pp.ppnl (Printer.pr_lconstr synthesized) ; flush stdout ;
print_endline "ENVIRONMENT:" ; flush stdout ;
Pp.ppnl (Printer.pr_context_of env) ; flush stdout ;
print_endline "FINE_ENVIRONMENT" ; flush stdout ;
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
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index 1de6a43252..578c1ed2f3 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -67,9 +67,9 @@ Pp.ppnl (Pp.str "Problem during the conversion of constr into XML") ;
Pp.ppnl (Pp.str "ENVIRONMENT:") ;
Pp.ppnl (Printer.pr_context_of rel_env) ;
Pp.ppnl (Pp.str "TERM:") ;
-Pp.ppnl (Printer.prterm_env rel_env obj') ;
+Pp.ppnl (Printer.pr_lconstr_env rel_env obj') ;
Pp.ppnl (Pp.str "RAW-TERM:") ;
-Pp.ppnl (Printer.prterm obj') ;
+Pp.ppnl (Printer.pr_lconstr obj') ;
Xml.xml_empty "MISSING TERM" [] (*; raise e*)
*)
;;
@@ -120,7 +120,7 @@ in
with _ ->
Pp.ppnl (Pp.(++) (Pp.str
"The_generated_term_is_not_a_subterm_of_the_final_lambda_term")
-(Printer.prterm constr)) ;
+(Printer.pr_lconstr constr)) ;
None
in
let rec aux node old_hyps =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 03:43:58 +0000