diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-09 15:33:28 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-09 15:33:28 +0000 |
| commit | e1723b1094719c1a60fddaa2668151b4f8ebc9ea (patch) | |
| tree | 992e8d5e42f3fa2983ded29d62486b4fd6bfa9c0 | |
| parent | 101f95e48a8bb7833ade978a12e3883a34d64235 (diff) | |
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
| -rw-r--r-- | tactics/equality.ml | 27 |
1 files 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 |