diff options
| author | herbelin | 2009-12-14 19:05:05 +0000 |
|---|---|---|
| committer | herbelin | 2009-12-14 19:05:05 +0000 |
| commit | cc5c3eb26f817a0a1cd479c0f7f3083e648b9a9b (patch) | |
| tree | d5de785d0560bb7c867560e8b09408b7f24a117e /tactics | |
| parent | f698148f6aee01a207ce5ddd4bebf19da2108bff (diff) | |
Improved strategy for rewriting lemma possibly depending because of evars.
Explained in CHANGES how to cope with the change of semantics of
abbreviations wrt implicit arguments positions propagation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12586 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index c6c29a5698..a82f506715 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -178,12 +178,6 @@ 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. *) -type substitutive_equality_flags = { - rewrite_dependent_proof : bool; - use_K : bool; - with_evars : bool -} - let find_elim hdcncl lft2rgt dep cls args gl = let inccl = (cls = None) in if (hdcncl = constr_of_reference (Coqlib.glob_eq) || @@ -221,7 +215,9 @@ let type_of_clause gl = function | Some id -> pf_get_hyp_typ gl id let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars dep_proof_ok gl hdcncl = - let dep = dep_proof_ok && occur_term c (type_of_clause gl cls) in + let isatomic = isProd (whd_zeta hdcncl) in + let dep_fun = if isatomic then dependent else dependent_no_evar in + let dep = dep_proof_ok && dep_fun c (type_of_clause gl cls) 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) |