From 898ac1e6654405a5a4ac31f4ca97acbe0c71c11c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 21 Aug 2007 10:18:46 +0000 Subject: [PATCH] Avoid confusion for names of proofs put in the applicative context. --- components/acic_content/acic2content.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/components/acic_content/acic2content.ml b/components/acic_content/acic2content.ml index 2c51fe7f8..b61cb1225 100644 --- a/components/acic_content/acic2content.ml +++ b/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 -- 2.39.2