From 058acfd867b172244c9beb95c11fdd2ad270f5a0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 30 Jul 2003 09:26:19 +0000 Subject: [PATCH] All the ids are now generated by gen_id. (Some of them were previously based on the acic ids). --- helm/ocaml/cic_omdoc/cic2content.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 = -- 2.39.2