From d83abd7e5e107f75b24e45dc75ad859ebc11c0fa Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 23 Aug 2007 20:54:05 +0000 Subject: [PATCH] Bug fixed: RewriteLR were not recognized correctly. Moreover they were also handled incorrectly (according to the is_top_down flag that should be irrelevant). --- helm/software/components/acic_content/acic2content.ml | 3 ++- helm/software/components/content_pres/content2pres.ml | 4 +--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml index b61cb1225..ddd1b5ebc 100644 --- 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 e25ff40d8..477697580 100644 --- 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 -- 2.39.2