From 8556f4e4b5e21535013e6962feabfede6313462b Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 11 Nov 2009 19:08:35 +0000 Subject: Backtracking on the use of automatically generated schemes for "eq"-rewriting (a few contributions are still referring explicitly to eq_rect, eq_ind and co and the new mechanism, though working also for dependent rewriting, is not powerful enough in general wrt fixpoint guard to claim being uniformly better). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12501 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/equality.ml | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/tactics/equality.ml b/tactics/equality.ml index f5e1fc5c43..abf2e51c4e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -176,8 +176,17 @@ let register_is_applied_rewrite_relation = (:=) is_applied_rewrite_relation (* find_elim determines which elimination principle is necessary to eliminate lbeq on sort_of_gl. *) -let find_elim hdcncl lft2rgt dep cls = + +let find_elim hdcncl lft2rgt dep cls gl = let inccl = (cls = None) in + if hdcncl = constr_of_reference (Coqlib.glob_eq) then + (* use eq_rect, eq_rect_r, etc for compatibility *) + let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in + let hdcncls = string_of_inductive hdcncl ^ suffix in + let rwr_thm = if lft2rgt = Some (cls=None) then hdcncls^"_r" else hdcncls in + try pf_global gl (id_of_string rwr_thm) + with Not_found -> error ("Cannot find rewrite principle "^rwr_thm^".") + else let scheme_name = match dep, lft2rgt, inccl with (* Non dependent case with symmetric equality *) | false, Some true, true | false, Some false, false -> rew_l2r_scheme_kind @@ -204,7 +213,7 @@ let type_of_clause gl = function let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars gl hdcncl = let dep = occur_term c (type_of_clause gl cls) in - let elim = find_elim hdcncl lft2rgt dep cls in + let elim = find_elim hdcncl lft2rgt dep cls gl in general_elim_clause with_evars tac cls sigma c t l (match lft2rgt with None -> false | Some b -> b) {elimindex = None; elimbody = (elim,NoBindings)} gl @@ -1080,7 +1089,7 @@ let swapEquandsInConcl gls = let bareRevSubstInConcl lbeq body (t,e1,e2) gls = (* find substitution scheme *) - let eq_elim = find_elim lbeq.eq (Some false) false None in + let eq_elim = find_elim lbeq.eq (Some false) false None gls in (* build substitution predicate *) let p = lambda_create (pf_env gls) (t,body) in (* apply substitution scheme *) -- cgit v1.2.3