Petit complément au commit 10131.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10136 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 4 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 320ea171fc..e046ee2fd8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -61,6 +61,9 @@ Tactic Language
   generated by expr_0. In this case, the value of expr (or idtac in
   case of just "..") is applied to the intermediate subgoals to make
   the number of tactics equal to the number of subgoals.
+- Names to be used as actual identifiers (like f in "apply f_equal f:=t")
+  must not be used elsewhere as variables in the same ltac expression
+  (possible source of incompatibility).
 
 Tactics
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index d276d2dd79..bb89756b30 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -375,6 +375,7 @@ let reduce_mind_case_use_function func env mia =
 	    fun i ->
 	      if i = bodynum then Some func
 	      else match names.(i) with
+		| Anonymous -> None
 		| Name id ->
 		    (* In case of a call to another component of a block of 
 		       mutual inductive, try to reuse the global name if