X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;h=2c46c3c46a23238d818740a18c2aec39642a7d96;hb=03d1ddf4a7fdf03fd497babd84d1963048253f0d;hp=0f23afb5691b7721b0b67b2f9e73ce267d3a9147;hpb=7fd0b9edc6be316b4ef43ca98a6b02f76dd1108e;p=helm.git

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