diff options
| author | Maxime Dénès | 2019-05-16 18:20:07 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-06-06 08:54:39 +0200 |
| commit | fb30e8880a3027ef1c957df668a906d723e8a8a0 (patch) | |
| tree | ad2825c374340dfa0bb4c8785034e689c0311d61 /vernac/metasyntax.mli | |
| parent | c0a695e89b0562eb6450c04ddba5e6e0414e5fd8 (diff) | |
`deprecated` attribute support for notations and syntactic definitions
We also slightly change the semantics of the `compat` syntax modifier to
re-express it in terms of the `deprecated` attribute, and we deprecate
it in favor of the latter.
Diffstat (limited to 'vernac/metasyntax.mli')
| -rw-r--r-- | vernac/metasyntax.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index 6435df23c7..6532cee367 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -19,10 +19,10 @@ val add_token_obj : string -> unit (** Adding a (constr) notation in the environment*) -val add_infix : locality_flag -> env -> (lstring * syntax_modifier list) -> +val add_infix : local:bool -> Deprecation.t option -> env -> (lstring * syntax_modifier list) -> constr_expr -> scope_name option -> unit -val add_notation : locality_flag -> env -> constr_expr -> +val add_notation : local:bool -> Deprecation.t option -> env -> constr_expr -> (lstring * syntax_modifier list) -> scope_name option -> unit val add_notation_extra_printing_rule : string -> string -> string -> unit @@ -47,12 +47,12 @@ val set_notation_for_interpretation : env -> Constrintern.internalization_env -> (** Add only the parsing/printing rule of a notation *) val add_syntax_extension : - locality_flag -> (lstring * syntax_modifier list) -> unit + local:bool -> (lstring * syntax_modifier list) -> unit (** Add a syntactic definition (as in "Notation f := ...") *) -val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr -> - bool -> Flags.compat_version option -> unit +val add_syntactic_definition : local:bool -> Deprecation.t option -> env -> + Id.t -> Id.t list * constr_expr -> Flags.compat_version option -> unit (** Print the Camlp5 state of a grammar *) |