From 9f282af121b609c4195389225130f3499fa31de2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 21 Sep 2007 14:29:20 +0000
Subject: Petit complément au commit 10131.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10136 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES             | 3 +++
 pretyping/tacred.ml | 1 +
 2 files changed, 4 insertions(+)

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
-- 
cgit v1.2.3