diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-19 17:48:11 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-19 19:08:54 +0100 |
| commit | 97e5a748bf921dc6cefae0041d2adb00f24f34cb (patch) | |
| tree | 44c44d2dbd4c5dd5116f2ce7fa3df964a7a3da54 /toplevel/vernacinterp.mli | |
| parent | ff26623a0b847149e6f119c98b7564d92710d59a (diff) | |
Adding a possible DEPRECATED flag to VERNAC EXTEND statements.
Diffstat (limited to 'toplevel/vernacinterp.mli')
| -rw-r--r-- | toplevel/vernacinterp.mli | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli index 38fce5d12..028206546 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -8,9 +8,13 @@ (** Interpretation of extended vernac phrases. *) -val vinterp_add : Vernacexpr.extend_name -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit +type deprecation = bool +type vernac_command = Genarg.raw_generic_argument list -> unit -> unit + +val vinterp_add : deprecation -> Vernacexpr.extend_name -> + vernac_command -> unit val overwriting_vinterp_add : - Vernacexpr.extend_name -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit + Vernacexpr.extend_name -> vernac_command -> unit val vinterp_init : unit -> unit val call : ?locality:bool -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit |