diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
commit | 1ef7f1c0c6897535a86daa77799714e25638f5e9 (patch) | |
tree | 5bcca733632ecc84d2c6b1ee48cb2e557a7adba5 /vernac/vernacinterp.ml | |
parent | 3a2fac7bcee36fd9dcb4f39a615c8ac0349abcc9 (diff) | |
parent | 9ebf44d84754adc5b64fcf612c6816c02c80462d (diff) |
Updated version 8.9.0 from 'upstream/8.9.0'
with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63
Diffstat (limited to 'vernac/vernacinterp.ml')
-rw-r--r-- | vernac/vernacinterp.ml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 1f2d2e4b..1bb1414f 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -12,15 +12,22 @@ open Util open Pp open CErrors -type deprecation = bool +type deprecation = { since : string option ; note : string option } + +let mk_deprecation ?(since=None) ?(note=None) () = + { since ; note } type atts = { loc : Loc.t option; locality : bool option; polymorphic : bool; program : bool; + deprecated : deprecation option; } +let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(program=false) ?(deprecated=None) () : atts = + { loc ; locality ; polymorphic ; program ; deprecated } + type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t type plugin_args = Genarg.raw_generic_argument list @@ -28,7 +35,7 @@ type plugin_args = Genarg.raw_generic_argument list (* Table of vernac entries *) let vernac_tab = (Hashtbl.create 211 : - (Vernacexpr.extend_name, deprecation * plugin_args vernac_command) Hashtbl.t) + (Vernacexpr.extend_name, bool * plugin_args vernac_command) Hashtbl.t) let vinterp_add depr s f = try @@ -79,7 +86,6 @@ let call opn converted_args ~atts ~st = phase := "Executing command"; hunk ~atts ~st with - | Drop -> raise Drop | reraise -> let reraise = CErrors.push reraise in if !Flags.debug then |