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.mli | |
| parent | d07b2862ec9a562f72c2f85e1b5f4529de200a07 (diff) | |
Add syntax for non maximally inserted implicit arguments
Diffstat (limited to 'vernac/comArguments.mli')
| -rw-r--r-- | vernac/comArguments.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comArguments.mli b/vernac/comArguments.mli index 71effddf67..cbc5fc15e2 100644 --- a/vernac/comArguments.mli +++ b/vernac/comArguments.mli @@ -12,6 +12,6 @@ val vernac_arguments : section_local:bool -> Libnames.qualid Constrexpr.or_by_notation -> Vernacexpr.vernac_argument_status list - -> (Names.Name.t * Impargs.implicit_kind) list list + -> (Names.Name.t * Glob_term.binding_kind) list list -> Vernacexpr.arguments_modifier list -> unit |