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

diff --git a/components/acic_content/acic2content.ml b/components/acic_content/acic2content.ml
index 99bab2de4..2c51fe7f8 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;
@@ -934,7 +938,11 @@ 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 then
+                  "RewriteLR"
+                 else
+                  "RewriteRL";
                 K.conclude_args = 
                   K.Term (false,(C.AConst (sid,uri,exp_named_subst)))::method_args;
                 K.conclude_conclusion =