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.ml | |
| parent | 8117f98527169955086332d771b1201b8f98cf31 (diff) | |
Make Environ.globals abstract.
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 0e34a7165..224b6d5b8 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -55,7 +55,8 @@ type globals = { 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} + env_modtypes : module_type_body MPmap.t; +} type stratification = { env_universes : UGraph.t; @@ -86,7 +87,7 @@ type rel_context_val = { } type env = { - 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; @@ -208,6 +209,9 @@ let lookup_named_val id env = let lookup_named_ctxt id ctxt = fst (Id.Map.find id ctxt.env_named_map) +let fold_constants f env acc = + Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_constants acc + (* Global constants *) let lookup_constant_key kn env = |