aboutsummaryrefslogtreecommitdiff
path: root/vernac/comArguments.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/comArguments.ml')
-rw-r--r--vernac/comArguments.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml
index 15077298aa..9d43debb77 100644
--- a/vernac/comArguments.ml
+++ b/vernac/comArguments.ml
@@ -228,7 +228,7 @@ let vernac_arguments ~section_local reference args more_implicits flags =
let implicits = List.map (List.map snd) implicits in
let implicits_specified = match implicits with
- | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l
+ | [l] -> List.exists (function Glob_term.Explicit -> false | _ -> true) l
| _ -> true in
if implicits_specified && clear_implicits_flag then