diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-03 22:27:09 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-03 22:27:09 +0000 |
| commit | add340bfaa3fed3ae77956c510c291ed4f9b8646 (patch) | |
| tree | 9c17eb825eeea6af65599e3e75c37c16eb6468aa /tactics/equality.ml | |
| parent | 66616778ed108dd21d1c9271f1d16e34048371e5 (diff) | |
Restored rewriting of JMeq using JMeq_rect and co when the domains are the same
(this was lost since revision 12481).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12560 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 1979a0494..f752e2cb3 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -176,11 +176,12 @@ 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 gl = +let find_elim hdcncl lft2rgt dep cls args gl = let inccl = (cls = None) in - if hdcncl = constr_of_reference (Coqlib.glob_eq) & not dep then - (* use eq_rect, eq_rect_r, etc for compatibility *) + if (hdcncl = constr_of_reference (Coqlib.glob_eq) || + hdcncl = constr_of_reference (Coqlib.glob_jmeq) && + pf_conv_x gl (List.nth args 0) (List.nth args 2)) && not dep then + (* use eq_rect, eq_rect_r, JMeq_rect, 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 @@ -213,7 +214,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 gl in + let elim = find_elim hdcncl lft2rgt dep cls (snd (decompose_app t)) 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 @@ -1089,7 +1090,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 gls in + let eq_elim = find_elim lbeq.eq (Some false) false None [e1;e2] gls in (* build substitution predicate *) let p = lambda_create (pf_env gls) (t,body) in (* apply substitution scheme *) |