Debugging stuff removed.

[helm.git] / helm / ocaml / cic_omdoc / cic2content.ml

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index e767b0f1980868e09c4563ff65b0fece071419f0..2c46c3c46a23238d818740a18c2aec39642a7d96 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -251,7 +251,7 @@ let generate_exact seed t id name ~ids_to_inner_types =
   let module C2A = Cic2acic in
   let module K = Content in
     { K.proof_name = name;
-      K.proof_id   = proof_prefix ^ id ;
+      K.proof_id   = gen_id proof_prefix seed ;
       K.proof_context = [] ;
       K.proof_apply_context = [];
       K.proof_conclude = 
@@ -271,7 +271,7 @@ let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_
   let module C = Cic in
   let module K = Content in
     { K.proof_name = name;
-      K.proof_id  = proof_prefix ^ id ;
+      K.proof_id  = gen_id proof_prefix seed ;
       K.proof_context = [] ;
       K.proof_apply_context = [];
       K.proof_conclude = 
@@ -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
@@ -834,30 +823,28 @@ let map_conjectures
  let context' =
   List.map
    (function
-       (id,None) as item -> item
+       (id,None) -> None
      | (id,Some (name,Cic.ADecl t)) ->
-         id,
-          Some
-           (* We should call build_decl_item, but we have not computed *)
-           (* the inner-types ==> we always produce a declaration      *)
-           (`Declaration
-             { K.dec_name = name_of name;
-               K.dec_id = gen_id declaration_prefix seed; 
-               K.dec_inductive = false;
-               K.dec_aref = get_id t;
-               K.dec_type = t
-             })
+         Some
+          (* We should call build_decl_item, but we have not computed *)
+          (* the inner-types ==> we always produce a declaration      *)
+          (`Declaration
+            { K.dec_name = name_of name;
+              K.dec_id = gen_id declaration_prefix seed; 
+              K.dec_inductive = false;
+              K.dec_aref = get_id t;
+              K.dec_type = t
+            })
      | (id,Some (name,Cic.ADef t)) ->
-         id,
-          Some
-           (* We should call build_def_item, but we have not computed *)
-           (* the inner-types ==> we always produce a declaration     *)
-           (`Definition
-              { K.def_name = name_of name;
-                K.def_id = gen_id definition_prefix seed; 
-                K.def_aref = get_id t;
-                K.def_term = t
-              })
+         Some
+          (* We should call build_def_item, but we have not computed *)
+          (* the inner-types ==> we always produce a declaration     *)
+          (`Definition
+             { K.def_name = name_of name;
+               K.def_id = gen_id definition_prefix seed; 
+               K.def_aref = get_id t;
+               K.def_term = t
+             })
    ) context
  in
   (id,n,context',ty)