From b993b6f15936219a54b2c057fc75ec1b8dde243a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 5 Sep 2003 10:59:02 +0000 Subject: [PATCH] Debugging infos removed. --- helm/ocaml/cic_omdoc/cic2content.ml | 21 +++++-------------- .../ocaml/cic_transformations/content2pres.ml | 3 --- 2 files changed, 5 insertions(+), 19 deletions(-) diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index 0f23afb56..2c46c3c46 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -405,27 +405,18 @@ build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types = let module K = Content in try let sort = Hashtbl.find ids_to_inner_sorts id in - (match name_of n with - Some "w" -> prerr_endline ("build_def: " ^ sort ); - | _ -> ()); if sort = "Prop" then - (prerr_endline ("entro"); - let p = + (let p = (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t) in - (match p.K.proof_name with - Some "w" -> prerr_endline ("TUTTO BENE:"); - | Some s -> prerr_endline ("mi chiamo " ^ s); - | _ -> prerr_endline ("ho perso il nome");); - prerr_endline ("esco"); `Proof p;) + `Proof p;) else - (prerr_endline ("siamo qui???"); `Definition { K.def_name = name_of n; K.def_id = gen_id definition_prefix seed; K.def_aref = id; K.def_term = t - }) + } with Not_found -> assert false @@ -705,7 +696,6 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = let subproofs,other_method_args = build_subproofs_and_args seed other_args ~ids_to_inner_types ~ids_to_inner_sorts in - prerr_endline "****** end other *******"; flush stderr; let method_args= let rec build_method_args = function @@ -725,8 +715,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = build_decl_item seed idl n s1 ~ids_to_inner_sorts in if (occur ind_uri s) then - ( prerr_endline ("inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr; - match t1 with + ( match t1 with Cic.ALambda(id2,n2,s2,t2) -> let inductive_hyp = `Hypothesis @@ -741,7 +730,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = (ce::inductive_hyp::context,body) | _ -> assert false) else - ( prerr_endline ("no inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr; + ( let (context,body) = bc (t,t1) in (ce::context,body)) | _ , t -> ([],aux t) in diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index e8699b8b4..a57ec0396 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -304,9 +304,6 @@ and proof2pres term2pres p = | None -> prerr_endline "NO NAME!!"; assert false) | `Proof p -> - (match p.Con.proof_name with - Some "w" -> prerr_endline ("processing w"); - | _ -> ()); proof2pres p | `Definition d -> (match d.Con.def_name with -- 2.39.2