aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/locality.ml20
-rw-r--r--vernac/locality.mli8
-rw-r--r--vernac/obligations.ml4
-rw-r--r--vernac/obligations.mli2
-rw-r--r--vernac/vernacentries.ml6
-rw-r--r--vernac/vernacinterp.ml18
-rw-r--r--vernac/vernacinterp.mli13
-rw-r--r--vernac/vernacstate.ml2
-rw-r--r--vernac/vernacstate.mli2
9 files changed, 30 insertions, 45 deletions
diff --git a/vernac/locality.ml b/vernac/locality.ml
index 054a451a46..681b1ab207 100644
--- a/vernac/locality.ml
+++ b/vernac/locality.ml
@@ -6,22 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
-
(** * Managing locality *)
let local_of_bool = function
| true -> Decl_kinds.Local
| false -> Decl_kinds.Global
-let check_locality locality_flag =
- match locality_flag with
- | Some b ->
- let s = if b then "Local" else "Global" in
- CErrors.user_err ~hdr:"Locality.check_locality"
- (str "This command does not support the \"" ++ str s ++ str "\" prefix.")
- | None -> ()
-
(** Extracting the locality flag *)
(* Commands which supported an inlined Local flag *)
@@ -95,13 +85,3 @@ let make_module_locality = function
let enforce_module_locality locality_flag local =
make_module_locality (enforce_locality_full locality_flag local)
-
-module LocalityFixme = struct
- let locality = ref None
- let set l = locality := l
- let consume () =
- let l = !locality in
- locality := None;
- l
- let assert_consumed () = check_locality !locality
-end
diff --git a/vernac/locality.mli b/vernac/locality.mli
index c1c45d6b0f..bef66d8bc5 100644
--- a/vernac/locality.mli
+++ b/vernac/locality.mli
@@ -41,11 +41,3 @@ val enforce_section_locality : bool option -> bool -> bool
val make_module_locality : bool option -> bool
val enforce_module_locality : bool option -> bool -> bool
-
-(* This is the old imperative interface that is still used for
- * VernacExtend vernaculars. Time permitting this could be trashed too *)
-module LocalityFixme : sig
- val set : bool option -> unit
- val consume : unit -> bool option
- val assert_consumed : unit -> unit
-end
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index a44de66e96..700fd6045b 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -155,7 +155,7 @@ let evar_dependencies evm oev =
let evi = Evd.find evm ev in
let deps' = evars_of_filtered_evar_info evi in
if Evar.Set.mem oev deps' then
- invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ string_of_existential oev)
+ invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev)
else Evar.Set.union deps' s)
deps deps
in
@@ -164,7 +164,7 @@ let evar_dependencies evm oev =
if Evar.Set.equal deps deps' then deps
else aux deps'
in aux (Evar.Set.singleton oev)
-
+
let move_after (id, ev, deps as obl) l =
let rec aux restdeps = function
| (id', _, _) as obl' :: tl ->
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 481faadb8e..0602e52e9a 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -32,7 +32,7 @@ val eterm_obligations : env -> Id.t -> evar_map -> int ->
(* Existential key, obl. name, type as product,
location of the original evar, associated tactic,
status and dependencies as indexes into the array *)
- * ((existential_key * Id.t) list * ((Id.t -> constr) -> constr -> constr)) *
+ * ((Evar.t * Id.t) list * ((Id.t -> constr) -> constr -> constr)) *
constr * types
(* Translations from existential identifiers to obligation identifiers
and for terms with existentials to closed terms, given a
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6191f37080..bdd351901d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -153,7 +153,7 @@ let show_match id =
let print_path_entry p =
let dir = DirPath.print (Loadpath.logical p) in
- let path = str (Loadpath.physical p) in
+ let path = str (CUnix.escaped_string_of_physical_path (Loadpath.physical p)) in
Pp.hov 2 (dir ++ spc () ++ path)
let print_loadpath dir =
@@ -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 *)
@@ -2144,7 +2144,7 @@ let vernac_timeout f =
match !current_timeout, !default_timeout with
| Some n, _ | None, Some n ->
let f () = f (); current_timeout := None in
- Control.timeout n f Timeout
+ Control.timeout n f () Timeout
| None, None -> f ()
let restore_timeout () = current_timeout := None
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 1d024386e2..47dec19588 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 =
@@ -66,10 +74,8 @@ let call ?locality ?loc (opn,converted_args) =
phase := "Checking arguments";
let hunk = callback converted_args in
phase := "Executing command";
- Locality.LocalityFixme.set locality;
- let res = hunk loc in
- Locality.LocalityFixme.assert_consumed ();
- res
+ let atts = { loc; locality } in
+ hunk ~atts
with
| Drop -> raise Drop
| reraise ->
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 1c66b1c045..602ccba157 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 9802a03cad..eb1359d52b 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 63a5b3b1eb..bcfa49aa38 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) *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 11:36:05 +0000