diff options
| author | SimonBoulier | 2019-12-02 12:52:39 +0100 |
|---|---|---|
| committer | SimonBoulier | 2020-02-04 16:07:21 +0100 |
| commit | a1d00fa77939f99dd5e7ddd41c8ecf64e8af4fa1 (patch) | |
| tree | 536f901c47c0080a5bc6a2d3b92adaefbfc8490f /vernac/comArguments.ml | |
| parent | d07b2862ec9a562f72c2f85e1b5f4529de200a07 (diff) | |
Add syntax for non maximally inserted implicit arguments
Diffstat (limited to 'vernac/comArguments.ml')
| -rw-r--r-- | vernac/comArguments.ml | 2 |
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 |