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

4 files changed, 14 insertions, 10 deletions

diff --git a/CHANGES b/CHANGES
index 9998364d9f..be86cd7ba6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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)