From e1723b1094719c1a60fddaa2668151b4f8ebc9ea Mon Sep 17 00:00:00 2001 From: msozeau Date: Wed, 9 Sep 2009 15:33:28 +0000 Subject: Stop trying to search if the relation is declared as a [RewriteRelation] before attempting generalized rewriting as the relation may itself be instantiated during the unification of the lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12312 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/equality.ml | 27 +++++++++++++-------------- 1 file changed, 13 insertions(+), 14 deletions(-) diff --git a/tactics/equality.ml b/tactics/equality.ml index 076f05f24..20e32bea3 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -208,20 +208,19 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ?tac leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c' (it_mkProd_or_LetIn t rels) l with_evars gl hdcncl | None -> - match !is_applied_rewrite_relation env sigma rels t with - | Some _ -> - rewrite_side_tac (!general_rewrite_clause cls - lft2rgt occs (c,l) ~new_goals:[]) tac gl - | None -> - let env' = push_rel_context rels env in - let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *) - match match_with_equality_type t' with - | Some (hdcncl,args) -> - let lft2rgt = adjust_rewriting_direction args lft2rgt in - leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c' - (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars gl hdcncl - | None -> - error "The provided term does not end with an equality or a declared rewrite relation." + try + rewrite_side_tac (!general_rewrite_clause cls + lft2rgt occs (c,l) ~new_goals:[]) tac gl + with e -> (* Try to see if there's an equality hidden *) + let env' = push_rel_context rels env in + let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *) + match match_with_equality_type t' with + | Some (hdcncl,args) -> + let lft2rgt = adjust_rewriting_direction args lft2rgt in + leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c' + (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars gl hdcncl + | None -> raise e + (* error "The provided term does not end with an equality or a declared rewrite relation." *) let general_rewrite_ebindings = general_rewrite_ebindings_clause None -- cgit v1.2.3