X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Facic_content%2Facic2content.ml;h=69a1f632dcf3117138c5b421dcfb94f9999adb10;hb=3e198ec27dc8f3a29cb2a64c7e0354006aa86352;hp=99bab2de44f122fc7d099ba331982bdbe7304409;hpb=190662b877ba89ccb152f0bf5c67df62be737335;p=helm.git

diff --git a/components/acic_content/acic2content.ml b/components/acic_content/acic2content.ml
index 99bab2de4..69a1f632d 100644
--- a/components/acic_content/acic2content.ml
+++ b/components/acic_content/acic2content.ml
@@ -118,7 +118,11 @@ let test_for_lifting ~ids_to_inner_types ~ids_to_inner_sorts=
   let module C2A = Cic2acic in
   (* atomic terms are never lifted, according to my policy *)
   function
-      C.ARel (id,_,_,_) -> false
+      C.ARel (id,_,_,_) ->
+         (try 
+            ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
+            true;
+          with Not_found -> false) 
     | C.AVar (id,_,_) -> 
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
@@ -356,7 +360,7 @@ let infer_dependent ~headless context metasenv = function
                   (n <> Cic.Anonymous && fstorder src, t) :: 
                   aux (CicSubstitution.subst 
                         (Deannotate.deannotate_term t) tgt) tl
-              | _ -> assert false
+              | _ -> List.map (fun s -> false,s) (t::tl)
        in
        (false, he) :: aux hety tl
      with CicTypeChecker.TypeCheckerFailure _ -> assert false
@@ -365,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;
@@ -440,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 
@@ -934,7 +941,12 @@ and rewrite seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_s
             K.proof_conclude = 
               { K.conclude_id = gen_id conclude_prefix seed; 
                 K.conclude_aref = id;
-                K.conclude_method = "Rewrite";
+                K.conclude_method =
+                 if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI
+                 || LibraryObjects.is_eq_ind_URI uri then
+                  "RewriteLR"
+                 else
+                  "RewriteRL";
                 K.conclude_args = 
                   K.Term (false,(C.AConst (sid,uri,exp_named_subst)))::method_args;
                 K.conclude_conclusion =