diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.ml | 1 | ||||
| -rw-r--r-- | API/API.mli | 65 |
2 files changed, 43 insertions, 23 deletions
diff --git a/API/API.ml b/API/API.ml index f588fe193a..78d9c0c26e 100644 --- a/API/API.ml +++ b/API/API.ml @@ -275,6 +275,7 @@ module Command = Command module Classes = Classes (* module Record *) (* module Assumptions *) +module Vernacstate = Vernacstate module Vernacinterp = Vernacinterp module Mltop = Mltop module Topfmt = Topfmt diff --git a/API/API.mli b/API/API.mli index cb945179f4..8a4a6cc891 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1863,6 +1863,9 @@ end module Nameops : sig + + open Names + val atompart_of_id : Names.Id.t -> string val pr_id : Names.Id.t -> Pp.t @@ -1871,19 +1874,28 @@ sig val pr_name : Names.Name.t -> Pp.t [@@ocaml.deprecated "alias of API.Names.Name.print"] - val name_fold : (Names.Id.t -> 'a -> 'a) -> Names.Name.t -> 'a -> 'a - val name_app : (Names.Id.t -> Names.Id.t) -> Names.Name.t -> Names.Name.t - val add_suffix : Names.Id.t -> string -> Names.Id.t - val increment_subscript : Names.Id.t -> Names.Id.t - val make_ident : string -> int option -> Names.Id.t - val out_name : Names.Name.t -> Names.Id.t - val pr_lab : Names.Label.t -> Pp.t - module Name : - sig - include module type of struct include Names.Name end + module Name : sig + include module type of struct include Name end + + val map : (Id.t -> Id.t) -> Name.t -> t val get_id : t -> Names.Id.t val fold_right : (Names.Id.t -> 'a -> 'a) -> t -> 'a -> 'a + end + + val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a + [@@ocaml.deprecated "alias of API.Names"] + + val name_app : (Id.t -> Id.t) -> Name.t -> Name.t + [@@ocaml.deprecated "alias of API.Names"] + + val add_suffix : Id.t -> string -> Id.t + val increment_subscript : Id.t -> Id.t + val make_ident : string -> int option -> Id.t + val out_name : Name.t -> Id.t + [@@ocaml.deprecated "alias of API.Names"] + val pr_lab : Label.t -> Pp.t + [@@ocaml.deprecated "alias of API.Names"] end module Libnames : @@ -5917,14 +5929,30 @@ sig Names.Id.t end +module Vernacstate : +sig + + type t = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) + } + + (* XXX: This should not be exported *) + val freeze_interp_state : Summary.marshallable -> t + val unfreeze_interp_state : t -> unit + +end + module Vernacinterp : sig + type deprecation = bool - type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit + type vernac_command = + Genarg.raw_generic_argument list -> Loc.t option -> Vernacstate.t -> Vernacstate.t - val vinterp_add : deprecation -> Vernacexpr.extend_name -> - vernac_command -> unit + val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit end @@ -5946,15 +5974,6 @@ end module Vernacentries : sig - type interp_state = { (* TODO: inline records in OCaml 4.03 *) - system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) - } - - val freeze_interp_state : Summary.marshallable -> interp_state - val unfreeze_interp_state : interp_state -> unit - val dump_global : Libnames.reference Misctypes.or_by_notation -> unit val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t @@ -5986,7 +6005,7 @@ sig val get_doc : Feedback.doc_id -> doc val state_of_id : doc:doc -> - Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ] + Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ] end (************************************************************************) |