aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/environ.ml66
-rw-r--r--kernel/environ.mli16
-rw-r--r--kernel/retypeops.ml1
-rw-r--r--kernel/safe_typing.ml4
-rw-r--r--kernel/safe_typing.mli2
5 files changed, 54 insertions, 35 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4a2aeea22d..98d66cafa1 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -50,12 +50,19 @@ type constant_key = Opaqueproof.opaque 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_inductives : mind_key Mindmap_env.t;
- env_modules : module_body MPmap.t;
- env_modtypes : module_type_body MPmap.t;
-}
+module Globals = struct
+
+ type view =
+ { constants : constant_key Cmap_env.t
+ ; inductives : mind_key Mindmap_env.t
+ ; modules : module_body MPmap.t
+ ; modtypes : module_type_body MPmap.t
+ }
+
+ type t = view
+
+ let view x = x
+end
type stratification = {
env_universes : UGraph.t;
@@ -88,7 +95,7 @@ type rel_context_val = {
}
type env = {
- env_globals : globals;
+ env_globals : Globals.t;
env_named_context : named_context_val; (* section variables *)
env_rel_context : rel_context_val;
env_nb_rel : int;
@@ -110,11 +117,12 @@ let empty_rel_context_val = {
}
let empty_env = {
- env_globals = {
- env_constants = Cmap_env.empty;
- env_inductives = Mindmap_env.empty;
- env_modules = MPmap.empty;
- env_modtypes = MPmap.empty};
+ env_globals =
+ { Globals.constants = Cmap_env.empty
+ ; inductives = Mindmap_env.empty
+ ; modules = MPmap.empty
+ ; modtypes = MPmap.empty
+ };
env_named_context = empty_named_context_val;
env_rel_context = empty_rel_context_val;
env_nb_rel = 0;
@@ -215,29 +223,29 @@ 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
+ Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.Globals.constants acc
let fold_inductives f env acc =
- Mindmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_inductives acc
+ Mindmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.Globals.inductives acc
(* Global constants *)
let lookup_constant_key kn env =
- Cmap_env.find kn env.env_globals.env_constants
+ Cmap_env.find kn env.env_globals.Globals.constants
let lookup_constant kn env =
- fst (Cmap_env.find kn env.env_globals.env_constants)
+ fst (Cmap_env.find kn env.env_globals.Globals.constants)
(* Mutual Inductives *)
let lookup_mind kn env =
- fst (Mindmap_env.find kn env.env_globals.env_inductives)
+ fst (Mindmap_env.find kn env.env_globals.Globals.inductives)
let mind_context env mind =
let mib = lookup_mind mind env in
Declareops.inductive_polymorphic_context mib
let lookup_mind_key kn env =
- Mindmap_env.find kn env.env_globals.env_inductives
+ Mindmap_env.find kn env.env_globals.Globals.inductives
let oracle env = env.env_typing_flags.conv_oracle
let set_oracle env o =
@@ -468,10 +476,10 @@ let no_link_info = NotLinked
let add_constant_key kn cb linkinfo env =
let new_constants =
- Cmap_env.add kn (cb,(ref linkinfo, ref None)) env.env_globals.env_constants in
+ Cmap_env.add kn (cb,(ref linkinfo, ref None)) env.env_globals.Globals.constants in
let new_globals =
{ env.env_globals with
- env_constants = new_constants } in
+ Globals.constants = new_constants } in
{ env with env_globals = new_globals }
let add_constant kn cb env =
@@ -598,10 +606,10 @@ let template_polymorphic_pind (ind,u) env =
else template_polymorphic_ind ind env
let add_mind_key kn (_mind, _ as mind_key) env =
- let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in
+ let new_inds = Mindmap_env.add kn mind_key env.env_globals.Globals.inductives in
let new_globals =
{ env.env_globals with
- env_inductives = new_inds; } in
+ Globals.inductives = new_inds; } in
{ env with env_globals = new_globals }
let add_mind kn mib env =
@@ -688,22 +696,22 @@ let keep_hyps env needed =
let add_modtype mtb env =
let mp = mtb.mod_mp in
- let new_modtypes = MPmap.add mp mtb env.env_globals.env_modtypes in
- let new_globals = { env.env_globals with env_modtypes = new_modtypes } in
+ let new_modtypes = MPmap.add mp mtb env.env_globals.Globals.modtypes in
+ let new_globals = { env.env_globals with Globals.modtypes = new_modtypes } in
{ env with env_globals = new_globals }
let shallow_add_module mb env =
let mp = mb.mod_mp in
- let new_mods = MPmap.add mp mb env.env_globals.env_modules in
- let new_globals = { env.env_globals with env_modules = new_mods } in
+ let new_mods = MPmap.add mp mb env.env_globals.Globals.modules in
+ let new_globals = { env.env_globals with Globals.modules = new_mods } in
{ env with env_globals = new_globals }
let lookup_module mp env =
- MPmap.find mp env.env_globals.env_modules
+ MPmap.find mp env.env_globals.Globals.modules
-let lookup_modtype mp env =
- MPmap.find mp env.env_globals.env_modtypes
+let lookup_modtype mp env =
+ MPmap.find mp env.env_globals.Globals.modtypes
(*s Judgments. *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f7de98dcfb..5af2a7288b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -46,8 +46,18 @@ type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key)
type mind_key = mutual_inductive_body * link_info ref
-type globals
-(** globals = constants + projections + inductive types + modules + module-types *)
+module Globals : sig
+ type t
+
+ type view =
+ { constants : constant_key Cmap_env.t
+ ; inductives : mind_key Mindmap_env.t
+ ; modules : module_body MPmap.t
+ ; modtypes : module_type_body MPmap.t
+ }
+
+ val view : t -> view
+end
type stratification = {
env_universes : UGraph.t;
@@ -67,7 +77,7 @@ type rel_context_val = private {
}
type env = private {
- env_globals : globals;
+ env_globals : Globals.t;
env_named_context : named_context_val; (* section variables *)
env_rel_context : rel_context_val;
env_nb_rel : int;
diff --git a/kernel/retypeops.ml b/kernel/retypeops.ml
index a51b762f95..f398e6a5da 100644
--- a/kernel/retypeops.ml
+++ b/kernel/retypeops.ml
@@ -71,6 +71,7 @@ let rec relevance_of_fterm env extra lft f =
| FLambda (len, tys, bdy, e) ->
let extra = List.rev_append (List.map (fun (x,_) -> binder_relevance x) tys) extra in
let lft = Esubst.el_liftn len lft in
+ let e = Esubst.subs_liftn len e in
relevance_of_term_extra env extra lft e bdy
| FLetIn (x, _, _, bdy, e) ->
relevance_of_term_extra env (x.binder_relevance :: extra)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fc55720583..98465c070b 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -320,10 +320,10 @@ let concat_private = SideEffects.concat
let universes_of_private eff =
let fold acc eff =
match eff.seff_body.const_universes with
- | Monomorphic ctx -> ctx :: acc
+ | Monomorphic ctx -> Univ.ContextSet.union ctx acc
| Polymorphic _ -> acc
in
- List.fold_left fold [] (side_effects_of_private_constants eff)
+ List.fold_left fold Univ.ContextSet.empty (side_effects_of_private_constants eff)
let env_of_safe_env senv = senv.env
let env_of_senv = env_of_safe_env
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 1b55293f1c..1ce790ebbb 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -59,7 +59,7 @@ val inline_private_constants :
val push_private_constants : Environ.env -> private_constants -> Environ.env
(** Push the constants in the environment if not already there. *)
-val universes_of_private : private_constants -> Univ.ContextSet.t list
+val universes_of_private : private_constants -> Univ.ContextSet.t
val is_curmod_library : safe_environment -> bool
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 17:08:30 +0000