* added test .html file for mozilla plugin

[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..0f23afb5691b7721b0b67b2f9e73ce267d3a9147 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 = 
@@ -834,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)