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/vernacexpr.ml | |
| parent | d07b2862ec9a562f72c2f85e1b5f4529de200a07 (diff) | |
Add syntax for non maximally inserted implicit arguments
Diffstat (limited to 'vernac/vernacexpr.ml')
| -rw-r--r-- | vernac/vernacexpr.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 1daa244986..22a8de7f99 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -254,7 +254,7 @@ type vernac_one_argument_status = { name : Name.t; recarg_like : bool; notation_scope : string CAst.t option; - implicit_status : Impargs.implicit_kind; + implicit_status : Glob_term.binding_kind; } type vernac_argument_status = @@ -386,7 +386,7 @@ type nonrec vernac_expr = | VernacArguments of qualid or_by_notation * vernac_argument_status list (* Main arguments status list *) * - (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) * + (Name.t * Glob_term.binding_kind) list list (* Extra implicit status lists *) * arguments_modifier list | VernacReserve of simple_binder list | VernacGeneralizable of (lident list) option |