From: Claudio Sacerdoti Coen Date: Thu, 23 Aug 2007 20:54:05 +0000 (+0000) Subject: Bug fixed: RewriteLR were not recognized correctly. Moreover they were also X-Git-Tag: make_still_working~6106 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d83abd7e5e107f75b24e45dc75ad859ebc11c0fa;p=helm.git 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 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