diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-01 19:53:57 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-01 19:53:57 +0000 |
commit | 80b91aa1e83097efd006cfed5f57e4826a1ab0c8 (patch) | |
tree | 75f2746f738c2b2c111b701f80d59d10f80c75f7 /plugins | |
parent | cf7660a3a8932ee593a376e8ec7ec251896a72e3 (diff) |
Cleaning Pp.ppnl use
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15413 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/omega/coq_omega.ml | 2 | ||||
-rw-r--r-- | plugins/romega/refl_omega.ml | 20 | ||||
-rw-r--r-- | plugins/xml/cic2acic.ml | 11 | ||||
-rw-r--r-- | plugins/xml/doubleTypeInference.ml | 4 | ||||
-rw-r--r-- | plugins/xml/proofTree2Xml.ml4 | 22 |
5 files changed, 14 insertions, 45 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index ddaf82a18..2a98cae53 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -509,7 +509,6 @@ 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.pr_lconstr t); failwith ("abstract_path " ^ string_of_int(List.length p)) in loop 1 path t @@ -530,7 +529,6 @@ 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.pr_lconstr t); failwith ("occurence " ^ string_of_int(List.length p)) in loop path t diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 550a4af2b..931ce400e 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -6,6 +6,7 @@ *************************************************************************) +open Pp open Errors open Util open Const_omega @@ -17,7 +18,7 @@ open OmegaSolver let debug = ref false let show_goal gl = - if !debug then Pp.ppnl (Tacmach.pr_gls gl); Tacticals.tclIDTAC gl + if !debug then (); Tacticals.tclIDTAC gl let pp i = print_int i; print_newline (); flush stdout @@ -160,16 +161,15 @@ let indice = function Left x | Right x -> x (* Affichage de l'environnement de réification (termes et propositions) *) let print_env_reification env = let rec loop c i = function - [] -> Printf.printf " ===============================\n\n" + [] -> str " ===============================\n\n" | t :: l -> - Printf.printf " (%c%02d) := " c i; - Pp.ppnl (Printer.pr_lconstr t); - Pp.flush_all (); - loop c (succ i) l in - print_newline (); - Printf.printf " ENVIRONMENT OF PROPOSITIONS :\n\n"; loop 'P' 0 env.props; - Printf.printf " ENVIRONMENT OF TERMS :\n\n"; loop 'V' 0 env.terms - + let s = Printf.sprintf "(%c%02d)" c i in + spc () ++ str s ++ str " := " ++ Printer.pr_lconstr t ++ fnl () ++ + loop c (succ i) l + in + let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in + let term_info = str "ENVIRONMENT OF TERMS :" ++ fnl () ++ loop 'V' 0 env.terms in + msg_debug (prop_info ++ fnl () ++ term_info) (* \subsection{Gestion des environnements de variable pour Omega} *) (* generation d'identifiant d'equation pour Omega *) diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index e29fcd0e8..62f7cc7cf 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -351,7 +351,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.pr_lconstr tt)) ; assert false +Pp.msg_debug (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. *) @@ -363,15 +363,6 @@ Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-ty (Termops.refresh_universes tt)) ; D.expected = None} in -(* Debugging only: -print_endline "TERMINE:" ; flush stdout ; -Pp.ppnl (Printer.pr_lconstr tt) ; flush stdout ; -print_endline "TIPO:" ; 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 ; -*) let innersort = let synthesized_innersort = get_sort_family_of env evar_map synthesized diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml index 24a383250..b1838f4a4 100644 --- a/plugins/xml/doubleTypeInference.ml +++ b/plugins/xml/doubleTypeInference.ml @@ -147,7 +147,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = (try Typeops.judge_of_type u with _ -> (* Successor of a non universe-variable universe anomaly *) - (Pp.ppnl (Pp.str "Warning: universe refresh performed!!!") ; flush stdout ) ; + Pp.msg_warning (Pp.str "Universe refresh performed!!!"); Typeops.judge_of_type (Termops.new_univ ()) ) @@ -239,7 +239,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.pr_lconstr cstr)) ; flush stdout ) ; + Pp.msg_warning (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.pr_lconstr cstr)); Acic.CicHash.add subterms_to_types cstr types ; E.make_judge cstr res diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4 index a45b8cda4..033e83410 100644 --- a/plugins/xml/proofTree2Xml.ml4 +++ b/plugins/xml/proofTree2Xml.ml4 @@ -56,16 +56,6 @@ let constr_to_xml obj sigma env = Errors.anomaly ("Problem during the conversion of constr into XML: " ^ Printexc.to_string e) -(* CSC: debugging stuff -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.pr_lconstr_env rel_env obj') ; -Pp.ppnl (Pp.str "RAW-TERM:") ; -Pp.ppnl (Printer.pr_lconstr obj') ; -Xml.xml_empty "MISSING TERM" [] (*; raise e*) -*) ;; let first_word s = @@ -98,20 +88,10 @@ let let module X = Xml in let ids_of_node node = let constr = Proof2aproof.ProofTreeHash.find proof_tree_to_constr node in -(* -let constr = - try - Proof2aproof.ProofTreeHash.find proof_tree_to_constr node - with _ -> Pp.ppnl (Pp.(++) (Pp.str "Node of the proof-tree that generated -no lambda-term: ") (Refiner.print_script true (Evd.empty) -(Global.named_context ()) node)) ; assert false (* Closed bug, should not -happen any more *) -in -*) try Some (Acic.CicHash.find constr_to_ids constr) with _ -> -Pp.ppnl (Pp.(++) (Pp.str +Pp.msg_warning (Pp.(++) (Pp.str "The_generated_term_is_not_a_subterm_of_the_final_lambda_term") (Printer.pr_lconstr constr)) ; None |