Bug fixed: RewriteLR were not recognized correctly. Moreover they were also

handled incorrectly (according to the is_top_down flag that should be irrelevant).

diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml
index b61cb1225e0cf4e9c997657ee9b4f7e87a210fba..ddd1b5ebcd02687a6d9a8834497fc9ebc984bf70 100644 (file)
--- a/helm/software/components/acic_content/acic2content.ml
+++ b/helm/software/components/acic_content/acic2content.ml
@@ -942,7 +942,8 @@ and rewrite seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_s
               { K.conclude_id = gen_id conclude_prefix seed; 
                 K.conclude_aref = id;
                 K.conclude_method =
-                 if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI then
+                 if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI
+                 || LibraryObjects.is_eq_ind_URI uri then
                   "RewriteLR"
                  else
                   "RewriteRL";

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index e25ff40d8ccb4ae51915bd0b0583774f8f7da24d..477697580fd4df83314ad345634a798b47870237 100644 (file)
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -449,9 +449,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (
         | Some j -> [j]
       in
       let index_term1, index_term2 =
-       if  (conclude.Con.conclude_method = "RewriteLR" && is_top_down)
-        || (conclude.Con.conclude_method = "RewriteRL" && not is_top_down)
-       then 2,5 else 5,2
+       if conclude.Con.conclude_method = "RewriteLR" then 2,5 else 5,2
       in
       let term1 = 
         (match List.nth conclude.Con.conclude_args index_term1 with