diff options
| author | Gaëtan Gilbert | 2019-11-20 16:27:09 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-20 16:27:09 +0100 |
| commit | 1248aed77ee36778cd440c14c4550dc97f78520b (patch) | |
| tree | 28a6ea3240a822fae58b5b5bc79b062247863fe7 /vernac/vernacexpr.ml | |
| parent | f37db0ff9b59720bb80433dff2995862550aec50 (diff) | |
make VernacArguments closer to user syntax
ie keep the fake arguments "/" and "&" instead of getting their index
at parsing time.
Diffstat (limited to 'vernac/vernacexpr.ml')
| -rw-r--r-- | vernac/vernacexpr.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 564c55670d..ce96d9265c 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -250,13 +250,17 @@ type vernac_cumulative = VernacCumulative | VernacNonCumulative (** {6 The type of vernacular expressions} *) -type vernac_argument_status = { +type vernac_one_argument_status = { name : Name.t; recarg_like : bool; notation_scope : string CAst.t option; implicit_status : Impargs.implicit_kind; } +type vernac_argument_status = + | VolatileArg | BidiArg + | RealArg of vernac_one_argument_status + type arguments_modifier = [ `Assert | `ClearBidiHint @@ -383,8 +387,6 @@ type nonrec vernac_expr = qualid or_by_notation * vernac_argument_status list (* Main arguments status list *) * (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) * - int option (* Number of args to trigger reduction *) * - int option (* Number of args before bidirectional typing *) * arguments_modifier list | VernacReserve of simple_binder list | VernacGeneralizable of (lident list) option |