diff options
| author | Maxime Dénès | 2016-10-28 09:29:25 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-10-28 09:29:25 +0200 |
| commit | 4f65c0370c5fc4163fa961a7fabb8e90fa7c45dd (patch) | |
| tree | 24a84ecb587edb6e14a1e1469f604239b7a6d6c2 /intf | |
| parent | d500a684be14b0c781ea4cda0ee02d3c5cdcad81 (diff) | |
| parent | ebb5bd7c2048daa7241bb07d8b53d07e0be27e62 (diff) | |
Merge remote-tracking branch 'github/pr/337' into v8.6
Was PR#337: Fix arguments
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 8572870407..1336c92b6f 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -416,10 +416,12 @@ type vernac_expr = | VernacDeclareImplicits of reference or_by_notation * (explicitation * bool * bool) list list | VernacArguments of reference or_by_notation * - (vernac_argument_status list) list * - int * [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | - `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | - `DefaultImplicits ] list + vernac_argument_status list (* Main arguments status list *) * + (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) * + int option (* Number of args to trigger reduction *) * + [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | + `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | + `DefaultImplicits ] list | VernacArgumentsScope of reference or_by_notation * scope_name option list | VernacReserve of simple_binder list @@ -479,11 +481,13 @@ and tacdef_body = | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) +and vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit + and vernac_argument_status = { name : Name.t; recarg_like : bool; notation_scope : (Loc.t * string) option; - implicit_status : [ `Implicit | `MaximallyImplicit | `NotImplicit]; + implicit_status : vernac_implicit_status; } (* A vernac classifier has to tell if a command: |