diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-06-29 10:05:56 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-29 10:05:56 +0200 |
commit | fc4f18c84bfc421dff55c77aa564abc1ea20f528 (patch) | |
tree | 4a9656e44d957f17a8c342e794a8bf2276ea50f3 /kernel/environ.mli | |
parent | 092b74035b73780432a1db9588a7ac54ec6a4721 (diff) | |
parent | e7e3714f0fd0e791501acccca3317ed8175c4815 (diff) |
Merge PR #7745: Make type Environ.globals abstract + simplify Environ.retroknowledge
Diffstat (limited to 'kernel/environ.mli')
-rw-r--r-- | kernel/environ.mli | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 8928b32f1..084d3c4de 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -46,13 +46,8 @@ type constant_key = constant_body * (link_info ref * key) type mind_key = mutual_inductive_body * link_info ref -type globals = { - env_constants : constant_key Cmap_env.t; - env_projections : projection_body Cmap_env.t; - env_inductives : mind_key Mindmap_env.t; - env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t -} +type globals +(** globals = constants + projections + inductive types + modules + module-types *) type stratification = { env_universes : UGraph.t; @@ -70,7 +65,7 @@ type rel_context_val = private { } type env = private { - env_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_globals : globals; env_named_context : named_context_val; (* section variables *) env_rel_context : rel_context_val; env_nb_rel : int; @@ -175,6 +170,9 @@ val reset_with_named_context : named_context_val -> env -> env (** This removes the [n] last declarations from the rel context *) val pop_rel_context : int -> env -> env +(** Useful for printing *) +val fold_constants : (Constant.t -> constant_body -> 'a -> 'a) -> env -> 'a -> 'a + (** {5 Global constants } {6 Add entries to global environment } *) @@ -320,6 +318,7 @@ open Retroknowledge (** functions manipulating the retroknowledge @author spiwack *) val retroknowledge : (retroknowledge->'a) -> env -> 'a +[@@ocaml.deprecated "Use the record projection."] val registered : env -> field -> bool |