All the ids are now generated by gen_id. (Some of them were previously based

on the acic ids).

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index e767b0f1980868e09c4563ff65b0fece071419f0..58ef34c871cd49cdc43c2302e73e4fa321c17ebf 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 =