diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-18 14:04:25 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-28 13:24:43 +0200 |
| commit | 3984f3c1db51f7b788ad49eafb7647774e8d1f53 (patch) | |
| tree | 5441491c9473f614ed5c648371f9114f19d2f80a /kernel/environ.mli | |
| parent | 8117f98527169955086332d771b1201b8f98cf31 (diff) | |
Make Environ.globals abstract.
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 8928b32f1..4c637bf78 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 } *) |