X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;h=0f23afb5691b7721b0b67b2f9e73ce267d3a9147;hb=f15a13bab100064a4da238cede323b8d4568c174;hp=335296effff7b374a7a4379f3d56a86828bcfff6;hpb=c1f6f44f9acab34668041aa85c6d6fbf7e6f9d55;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 335296eff..0f23afb56 100644
--- 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 = 
@@ -671,6 +671,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
           if (uri_str = "cic:/Coq/Init/Logic_Type/exT_ind.con" or
               uri_str = "cic:/Coq/Init/Logic/ex_ind.con") then "Exists"
           else if uri_str = "cic:/Coq/Init/Logic/and_ind.con" then "AndInd"
+          else if uri_str = "cic:/Coq/Init/Logic/False_ind.con" then "FalseInd"
           else "ByInduction" in
         let prefix = String.sub uri_str 0 n in
         let ind_str = (prefix ^ ".ind") in 
@@ -687,9 +688,6 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
           let p,a = split (n-1) (List.tl l) in
           ((List.hd l::p),a) in
         let params_and_IP,tail_args = split (noparams+1) args in
-        if method_name = "Exists" then
-          (prerr_endline ("+++++args++++:" ^ string_of_int (List.length args));
-           prerr_endline ("+++++tail++++:" ^ string_of_int (List.length tail_args)));
         let constructors = 
             (match inductive_types with
               [(_,_,_,l)] -> l
@@ -836,30 +834,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)