diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 1 |
2 files changed, 4 insertions, 0 deletions
@@ -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 |