In order to generate executable declarative scripts, we are now splitting

[helm.git] / helm / software / components / acic_content / acic2content.ml

diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml
index f27b881ba888a68653bb2393f6168d03084f6f8f..2c51fe7f80331d23c800fdab42fa9dc78e073bd2 100644 (file)
--- a/helm/software/components/acic_content/acic2content.ml
+++ b/helm/software/components/acic_content/acic2content.ml
@@ -938,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 =