From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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