diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/tacred.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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 |