From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 30 Jul 2003 09:26:19 +0000 (+0000)
Subject: All the ids are now generated by gen_id. (Some of them were previously based
X-Git-Tag: LucaOK~12
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=058acfd867b172244c9beb95c11fdd2ad270f5a0;p=helm.git

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 e767b0f19..58ef34c87 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 =