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/xml/proofTree2Xml.ml4 | |
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/xml/proofTree2Xml.ml4')
-rw-r--r-- | plugins/xml/proofTree2Xml.ml4 | 22 |
1 files changed, 1 insertions, 21 deletions
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 |