From: Claudio Sacerdoti Coen Date: Tue, 21 Aug 2007 10:18:46 +0000 (+0000) Subject: Avoid confusion for names of proofs put in the applicative context. X-Git-Tag: make_still_working~6110 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b73c1560045798ff1e77491050409a783d915345;p=helm.git Avoid confusion for names of proofs put in the applicative context. --- diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml index 2c51fe7f8..b61cb1225 100644 --- a/helm/software/components/acic_content/acic2content.ml +++ b/helm/software/components/acic_content/acic2content.ml @@ -369,16 +369,19 @@ let infer_dependent ~headless context metasenv = function let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_to_inner_types ~ids_to_inner_sorts = let module C = Cic in let module K = Content in - let rec aux = + let rec aux n = function [] -> [],[] | (dep, t)::l1 -> - let subproofs,args = aux l1 in - if (test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts) then + let need_lifting = + test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts in + let subproofs,args = aux (n + if need_lifting then 1 else 0) l1 in + if need_lifting then let new_subproof = acic2content seed context metasenv - ~name:"H" ~ids_to_inner_types ~ids_to_inner_sorts t in + ~name:("H" ^ string_of_int n) ~ids_to_inner_types + ~ids_to_inner_sorts t in let new_arg = K.Premise { K.premise_id = gen_id premise_prefix seed; @@ -444,7 +447,7 @@ let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_ | _ -> (K.Term (dep,t))) in subproofs,hd::args in - match (aux (infer_dependent ~headless context metasenv l)) with + match (aux 1 (infer_dependent ~headless context metasenv l)) with [p],args -> [{p with K.proof_name = None}], List.map