diff options
| author | Maxime Dénès | 2016-10-24 01:25:40 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-10-27 10:12:55 +0200 |
| commit | 5da679d276e106a62cc3368ceb7358da289ea10a (patch) | |
| tree | 6dc390761cfe8ef2ab5ae9537a5c0a9266d4e289 /intf | |
| parent | 7c047370dc9032e3ded3365a45de5b92e7c9033f (diff) | |
Complete overhaul of the Arguments vernacular.
The main point of this change is to fix #3035: Avoiding trailing
arguments in the Arguments command, and related issues occurring in
HoTT for instance. When the "assert" flag is not specified, we now
accept prefixes of the list of arguments.
The semantics of _ w.r.t. to renaming has changed. Previously, it meant
"restore the original name inferred from the type". Now it means "don't
change the current name".
The syntax of arguments is now restricted. Modifiers like /, ! and
scopes are allowed only in the first arguments list.
We also add *a lot* of missing checks on input values and fix various
bugs.
Note that this code is still way too complex for what it does, due to
the complexity of the implicit arguments, reduction behaviors and renaming
APIs.
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: |