Debugging infos removed.

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 0f23afb5691b7721b0b67b2f9e73ce267d3a9147..2c46c3c46a23238d818740a18c2aec39642a7d96 100644 (file)
--- 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 e8699b8b4445d24f04d585b6c7c21dbbcbb18ada..a57ec0396731758266625b10a726370e820b6197 100644 (file)
--- 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