diff options
Diffstat (limited to 'vernac/comArguments.ml')
| -rw-r--r-- | vernac/comArguments.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml index be9cc059a7..adf1f42beb 100644 --- a/vernac/comArguments.ml +++ b/vernac/comArguments.ml @@ -218,9 +218,8 @@ let vernac_arguments ~section_local reference args more_implicits flags = in let implicits = implicits :: more_implicits in - let implicits = List.map (List.map snd) implicits in let implicits_specified = match implicits with - | [l] -> List.exists (function Glob_term.Explicit -> false | _ -> true) l + | [l] -> List.exists (function _, Glob_term.Explicit -> false | _ -> true) l | _ -> true in if implicits_specified && clear_implicits_flag then |