diff options
Diffstat (limited to 'vernac')
-rw-r--r-- | vernac/vernacentries.ml | 2 | ||||
-rw-r--r-- | vernac/vernacinterp.ml | 15 | ||||
-rw-r--r-- | vernac/vernacinterp.mli | 13 | ||||
-rw-r--r-- | vernac/vernacstate.ml | 2 | ||||
-rw-r--r-- | vernac/vernacstate.mli | 2 |
5 files changed, 25 insertions, 9 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 10c139e5a..358e965ec 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2078,7 +2078,7 @@ let interp ?proof ?loc locality poly st c = (* Extensions *) | VernacExtend (opn,args) -> (* XXX: Here we are returning the state! :) *) - let _st : Vernacstate.t = Vernacinterp.call ?locality ?loc (opn,args) st in + let _st : Vernacstate.t = Vernacinterp.call ?locality ?loc (opn,args) ~st in () (* Vernaculars that take a locality flag *) diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 1d024386e..725436fef 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -11,8 +11,16 @@ open Pp open CErrors type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> - Vernacstate.t -> Vernacstate.t + +type atts = { + loc : Loc.t option; + locality : bool option; +} + +type vernac_command = + Genarg.raw_generic_argument list -> + atts:atts -> st:Vernacstate.t -> + Vernacstate.t (* Table of vernac entries *) let vernac_tab = @@ -67,7 +75,8 @@ let call ?locality ?loc (opn,converted_args) = let hunk = callback converted_args in phase := "Executing command"; Locality.LocalityFixme.set locality; - let res = hunk loc in + let atts = { loc; locality } in + let res = hunk ~atts in Locality.LocalityFixme.assert_consumed (); res with diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli index 1c66b1c04..602ccba15 100644 --- a/vernac/vernacinterp.mli +++ b/vernac/vernacinterp.mli @@ -10,8 +10,15 @@ type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> - Vernacstate.t -> Vernacstate.t +type atts = { + loc : Loc.t option; + locality : bool option; +} + +type vernac_command = + Genarg.raw_generic_argument list -> + atts:atts -> st:Vernacstate.t -> + Vernacstate.t val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit @@ -21,4 +28,4 @@ val vinterp_init : unit -> unit val call : ?locality:bool -> ?loc:Loc.t -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> - Vernacstate.t -> Vernacstate.t + st:Vernacstate.t -> Vernacstate.t diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 9802a03ca..eb1359d52 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -type t = { (* TODO: inline records in OCaml 4.03 *) +type t = { system : States.state; (* summary + libstack *) proof : Proof_global.state; (* proof state *) shallow : bool (* is the state trimmed down (libstack) *) diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index 63a5b3b1e..bcfa49aa3 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -type t = { (* TODO: inline records in OCaml 4.03 *) +type t = { system : States.state; (* summary + libstack *) proof : Proof_global.state; (* proof state *) shallow : bool (* is the state trimmed down (libstack) *) |