diff options
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 7 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 1 | ||||
| -rw-r--r-- | tactics/equality.ml | 10 |
4 files changed, 14 insertions, 10 deletions
@@ -63,8 +63,10 @@ Notations - Abbreviations now use implicit arguments and arguments scopes for printing. - Abbreviations to pure names now strictly behave like the name they refer to (make redirections of qualified names easier). -- Abbreviations to applied names now propagate the implicit arguments and - arguments scope of the underlying reference. +- Abbreviations for applied constant now propagate the implicit arguments + and arguments scope of the underlying reference (possible source of + incompatibilities generally solvable by changing such abbreviations from + e.g. "Notation foo' := (foo x)" to "Notation foo' y := (foo x (y:=y))"). - The "where" clause now supports multiple notations per defined object. Vernacular commands diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index bbc0ceae7d..d5bc868894 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -219,6 +219,7 @@ open RedFlags (* Local *) let beta = mkflags [fbeta] let eta = mkflags [feta] +let zeta = mkflags [fzeta] let betaiota = mkflags [fiota; fbeta] let betaiotazeta = mkflags [fiota; fbeta;fzeta] @@ -495,10 +496,14 @@ let whd_betadeltaiota_nolet_stack env = let whd_betadeltaiota_nolet env = red_of_state_red (whd_betadeltaiota_nolet_state env) -(* 3. Eta reduction Functions *) +(* 4. Eta reduction Functions *) let whd_eta c = app_stack (local_whd_state_gen eta Evd.empty (c,empty_stack)) +(* 5. Zeta Reduction Functions *) + +let whd_zeta c = app_stack (local_whd_state_gen zeta Evd.empty (c,empty_stack)) + (****************************************************************************) (* Reduction Functions *) (****************************************************************************) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 1268a3f3b5..9e5ced8a28 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -136,6 +136,7 @@ val whd_betadeltaiotaeta_state : state_reduction_function val whd_betadeltaiotaeta : reduction_function val whd_eta : constr -> constr +val whd_zeta : constr -> constr (* Various reduction functions *) 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) |