aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cooking.ml10
-rw-r--r--kernel/cooking.mli2
-rw-r--r--kernel/entries.ml8
-rw-r--r--kernel/opaqueproof.ml97
-rw-r--r--kernel/opaqueproof.mli18
-rw-r--r--kernel/safe_typing.ml65
-rw-r--r--kernel/section.ml24
-rw-r--r--kernel/term_typing.ml28
8 files changed, 111 insertions, 141 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 0951b07d49..fae06f7163 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -161,7 +161,7 @@ type 'opaque result = {
cook_universes : universes;
cook_relevance : Sorts.relevance;
cook_inline : inline;
- cook_context : Constr.named_context option;
+ cook_context : Id.Set.t option;
}
let expmod_constr_subst cache modlist subst c =
@@ -239,14 +239,10 @@ let cook_constant { from = cb; info } =
| Undef _ as x -> x
| Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs)))
| OpaqueDef o ->
- OpaqueDef (Opaqueproof.discharge_direct_opaque info o)
+ OpaqueDef (Opaqueproof.discharge_opaque info o)
| Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
in
- let const_hyps =
- Context.Named.fold_outside (fun decl hyps ->
- List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl')))
- hyps)
- hyps0 ~init:cb.const_hyps in
+ let const_hyps = Id.Set.diff (Context.Named.to_vars cb.const_hyps) (Context.Named.to_vars hyps0) in
let typ = abstract_constant_type (expmod cb.const_type) hyps in
{
cook_body = body;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 671cdf51fe..83a8b9edfc 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -23,7 +23,7 @@ type 'opaque result = {
cook_universes : universes;
cook_relevance : Sorts.relevance;
cook_inline : inline;
- cook_context : Constr.named_context option;
+ cook_context : Names.Id.Set.t option;
}
val cook_constant : recipe -> Opaqueproof.opaque result
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 47e2f72b0e..1e6bc14935 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -61,7 +61,7 @@ type mutual_inductive_entry = {
type definition_entry = {
const_entry_body : constr;
(* List of section variables *)
- const_entry_secctx : Constr.named_context option;
+ const_entry_secctx : Id.Set.t option;
(* State id on which the completion of type checking is reported *)
const_entry_feedback : Stateid.t option;
const_entry_type : types option;
@@ -70,7 +70,7 @@ type definition_entry = {
type section_def_entry = {
secdef_body : constr;
- secdef_secctx : Constr.named_context option;
+ secdef_secctx : Id.Set.t option;
secdef_feedback : Stateid.t option;
secdef_type : types option;
}
@@ -78,7 +78,7 @@ type section_def_entry = {
type 'a opaque_entry = {
opaque_entry_body : 'a;
(* List of section variables *)
- opaque_entry_secctx : Constr.named_context;
+ opaque_entry_secctx : Id.Set.t;
(* State id on which the completion of type checking is reported *)
opaque_entry_feedback : Stateid.t option;
opaque_entry_type : types;
@@ -88,7 +88,7 @@ type 'a opaque_entry = {
type inline = int option (* inlining level, None for no inlining *)
type parameter_entry =
- Constr.named_context option * types in_universes_entry * inline
+ Id.Set.t option * types in_universes_entry * inline
type primitive_entry = {
prim_entry_type : types option;
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index f0ffd2e073..f0b706e4f5 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -24,7 +24,7 @@ type 'a delayed_universes =
| PrivateMonomorphic of 'a
| PrivatePolymorphic of int * Univ.ContextSet.t
-type opaque_proofterm = cooking_info list * (Constr.t * unit delayed_universes) option
+type opaque_proofterm = (Constr.t * unit delayed_universes) option
type indirect_accessor = {
access_proof : DirPath.t -> int -> opaque_proofterm;
@@ -38,10 +38,10 @@ let drop_mono = function
type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation
type opaque =
- | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
- | Direct of cooking_info list * proofterm
+| Indirect of substitution list * cooking_info list * DirPath.t * int (* subst, discharge, lib, index *)
+
type opaquetab = {
- opaque_val : (cooking_info list * proofterm) Int.Map.t;
+ opaque_val : proofterm Int.Map.t;
(** Actual proof terms *)
opaque_len : int;
(** Size of the above map *)
@@ -56,44 +56,33 @@ let empty_opaquetab = {
let not_here () =
CErrors.user_err Pp.(str "Cannot access opaque delayed proof")
-let create cu = Direct ([],cu)
-
-let turn_indirect dp o tab = match o with
- | Indirect (_,_,i) ->
- if not (Int.Map.mem i tab.opaque_val)
- then CErrors.anomaly (Pp.str "Indirect in a different table.")
- else CErrors.anomaly (Pp.str "Already an indirect opaque.")
- | Direct (d, cu) ->
- (* Invariant: direct opaques only exist inside sections, we turn them
- indirect as soon as we are at toplevel. At this moment, we perform
- hashconsing of their contents, potentially as a future. *)
- let hcons (c, u) =
- let c = Constr.hcons c in
- let u = match u with
- | PrivateMonomorphic u -> PrivateMonomorphic (Univ.hcons_universe_context_set u)
- | PrivatePolymorphic (n, u) -> PrivatePolymorphic (n, Univ.hcons_universe_context_set u)
- in
- (c, u)
- in
- let cu = Future.chain cu hcons in
- let id = tab.opaque_len in
- let opaque_val = Int.Map.add id (d,cu) tab.opaque_val in
- let opaque_dir =
- if DirPath.equal dp tab.opaque_dir then tab.opaque_dir
- else if DirPath.equal tab.opaque_dir DirPath.initial then dp
- else CErrors.anomaly
- (Pp.str "Using the same opaque table for multiple dirpaths.") in
- let ntab = { opaque_val; opaque_dir; opaque_len = id + 1 } in
- Indirect ([],dp,id), ntab
+let create dp cu tab =
+ let hcons (c, u) =
+ let c = Constr.hcons c in
+ let u = match u with
+ | PrivateMonomorphic u -> PrivateMonomorphic (Univ.hcons_universe_context_set u)
+ | PrivatePolymorphic (n, u) -> PrivatePolymorphic (n, Univ.hcons_universe_context_set u)
+ in
+ (c, u)
+ in
+ let cu = Future.chain cu hcons in
+ let id = tab.opaque_len in
+ let opaque_val = Int.Map.add id cu tab.opaque_val in
+ let opaque_dir =
+ if DirPath.equal dp tab.opaque_dir then tab.opaque_dir
+ else if DirPath.equal tab.opaque_dir DirPath.initial then dp
+ else CErrors.anomaly
+ (Pp.str "Using the same opaque table for multiple dirpaths.") in
+ let ntab = { opaque_val; opaque_dir; opaque_len = id + 1 } in
+ Indirect ([], [], dp, id), ntab
let subst_opaque sub = function
- | Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
- | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.")
+| Indirect (s, ci, dp, i) -> Indirect (sub :: s, ci, dp, i)
-let discharge_direct_opaque ci = function
- | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
- | Direct (d, cu) ->
- Direct (ci :: d, cu)
+let discharge_opaque info = function
+| Indirect (s, ci, dp, i) ->
+ assert (CList.is_empty s);
+ Indirect ([], info :: ci, dp, i)
let join except cu = match except with
| None -> ignore (Future.join cu)
@@ -102,25 +91,21 @@ let join except cu = match except with
else ignore (Future.join cu)
let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
- | Direct (_,cu) -> join except cu
- | Indirect (_,dp,i) ->
- if DirPath.equal dp odp then
- let (_, fp) = Int.Map.find i prfs in
- join except fp
+| Indirect (_,_,dp,i) ->
+ if DirPath.equal dp odp then
+ let fp = Int.Map.find i prfs in
+ join except fp
let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
- | Direct (d, cu) ->
- let (c, u) = Future.force cu in
- access.access_discharge d (c, drop_mono u)
- | Indirect (l,dp,i) ->
+ | Indirect (l,d,dp,i) ->
let c, u =
if DirPath.equal dp odp
then
- let (d, cu) = Int.Map.find i prfs in
+ let cu = Int.Map.find i prfs in
let (c, u) = Future.force cu in
access.access_discharge d (c, drop_mono u)
else
- let (d, cu) = access.access_proof dp i in
+ let cu = access.access_proof dp i in
match cu with
| None -> not_here ()
| Some (c, u) -> access.access_discharge d (c, u)
@@ -133,21 +118,19 @@ let get_mono (_, u) = match u with
| PrivatePolymorphic _ -> Univ.ContextSet.empty
let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function
- | Direct (_,cu) ->
- get_mono (Future.force cu)
- | Indirect (_,dp,i) ->
+| Indirect (_,_,dp,i) ->
if DirPath.equal dp odp
then
- let ( _, cu) = Int.Map.find i prfs in
+ let cu = Int.Map.find i prfs in
get_mono (Future.force cu)
else Univ.ContextSet.empty
module FMap = Future.UUIDMap
let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } =
- let opaque_table = Array.make n ([], None) in
+ let opaque_table = Array.make n None in
let f2t_map = ref FMap.empty in
- let iter n (d, cu) =
+ let iter n cu =
let uid = Future.uuid cu in
let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
let c =
@@ -160,7 +143,7 @@ let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _
CErrors.anomaly
Pp.(str"Proof object "++int n++str" is not checked nor to be checked")
in
- opaque_table.(n) <- (d, c)
+ opaque_table.(n) <- c
in
let () = Int.Map.iter iter otab in
opaque_table, !f2t_map
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 758a9f5107..1870241dcd 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -16,10 +16,7 @@ open Mod_subst
Opaque proof terms are special since:
- they can be lazily computed and substituted
- they are stored in an optionally loaded segment of .vo files
- An [opaque] proof terms holds the real data until fully discharged.
- In this case it is called [direct].
- When it is [turn_indirect] the data is relocated to an opaque table
- and the [opaque] is turned into an index. *)
+ An [opaque] proof terms holds an index into an opaque table. *)
type 'a delayed_universes =
| PrivateMonomorphic of 'a
@@ -33,12 +30,7 @@ type opaque
val empty_opaquetab : opaquetab
(** From a [proofterm] to some [opaque]. *)
-val create : proofterm -> opaque
-
-(** Turn a direct [opaque] into an indirect one. It is your responsibility to
- hashcons the inner term beforehand. The integer is an hint of the maximum id
- used so far *)
-val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
+val create : DirPath.t -> proofterm -> opaquetab -> opaque * opaquetab
type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
(Univ.Instance.t * Id.t array) Mindmap.t
@@ -47,14 +39,14 @@ type cooking_info = {
modlist : work_list;
abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
-type opaque_proofterm = cooking_info list * (Constr.t * unit delayed_universes) option
+type opaque_proofterm = (Constr.t * unit delayed_universes) option
type indirect_accessor = {
access_proof : DirPath.t -> int -> opaque_proofterm;
access_discharge : cooking_info list ->
(Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes);
}
-(** When stored indirectly, opaque terms are indexed by their library
+(** Opaque terms are indexed by their library
dirpath and an integer index. The two functions above activate
this indirect storage, by telling how to retrieve terms.
*)
@@ -66,7 +58,7 @@ val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.Context
val subst_opaque : substitution -> opaque -> opaque
-val discharge_direct_opaque :
+val discharge_opaque :
cooking_info -> opaque -> opaque
val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 4268f0a602..9b4d2e69ac 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -591,17 +591,6 @@ let add_constant_aux ~in_section senv (kn, cb) =
let l = Constant.label kn in
(* This is the only place where we hashcons the contents of a constant body *)
let cb = if in_section then cb else Declareops.hcons_const_body cb in
- let cb, otab = match cb.const_body with
- | OpaqueDef lc when not in_section ->
- (* In coqc, opaque constants outside sections will be stored
- indirectly in a specific table *)
- let od, otab =
- Opaqueproof.turn_indirect
- (library_dp_of_senv senv) lc (Environ.opaque_tables senv.env) in
- { cb with const_body = OpaqueDef od }, otab
- | _ -> cb, (Environ.opaque_tables senv.env)
- in
- let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in
let senv' = add_field (l,SFBconst cb) (C kn) senv in
let senv'' = match cb.const_body with
| Undef (Some lev) ->
@@ -733,7 +722,7 @@ let constant_entry_of_side_effect eff =
if Declareops.is_opaque cb then
OpaqueEff {
opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
- opaque_entry_secctx = cb.const_hyps;
+ opaque_entry_secctx = Context.Named.to_vars cb.const_hyps;
opaque_entry_feedback = None;
opaque_entry_type = cb.const_type;
opaque_entry_universes = univs;
@@ -741,7 +730,7 @@ let constant_entry_of_side_effect eff =
else
DefinitionEff {
const_entry_body = p;
- const_entry_secctx = Some cb.const_hyps;
+ const_entry_secctx = Some (Context.Named.to_vars cb.const_hyps);
const_entry_feedback = None;
const_entry_type = Some cb.const_type;
const_entry_universes = univs;
@@ -805,17 +794,25 @@ let export_side_effects mb env (b_ctx, eff) =
in
translate_seff trusted seff [] env
+let push_opaque_proof pf senv =
+ let o, otab = Opaqueproof.create (library_dp_of_senv senv) pf (Environ.opaque_tables senv.env) in
+ let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in
+ senv, o
+
let export_private_constants ~in_section ce senv =
let exported, ce = export_side_effects senv.revstruct senv.env ce in
- let map univs p =
- let local = match univs with
+ let map senv (kn, c) = match c.const_body with
+ | OpaqueDef p ->
+ let local = match c.const_universes with
| Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty
| Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty)
in
- Opaqueproof.create (Future.from_val (p, local))
+ let senv, o = push_opaque_proof (Future.from_val (p, local)) senv in
+ senv, (kn, { c with const_body = OpaqueDef o })
+ | Def _ | Undef _ | Primitive _ as body ->
+ senv, (kn, { c with const_body = body })
in
- let map (kn, cb) = (kn, map_constant (fun c -> map cb.const_universes c) cb) in
- let bodies = List.map map exported in
+ let senv, bodies = List.fold_left_map map senv exported in
let exported = List.map (fun (kn, _) -> kn) exported in
(* No delayed constants to declare *)
let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
@@ -836,20 +833,25 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
Term_typing.translate_constant Term_typing.Pure senv.env kn ce
in
let senv =
- let delayed_cst = match cb.const_body with
- | OpaqueDef fc when not (Declareops.constant_is_polymorphic cb) ->
- let map (_, u) = match u with
- | Opaqueproof.PrivateMonomorphic ctx -> ctx
- | Opaqueproof.PrivatePolymorphic _ -> assert false
+ let senv, cb, delayed_cst = match cb.const_body with
+ | OpaqueDef fc ->
+ let senv, o = push_opaque_proof fc senv in
+ let delayed_cst =
+ if not (Declareops.constant_is_polymorphic cb) then
+ let map (_, u) = match u with
+ | Opaqueproof.PrivateMonomorphic ctx -> ctx
+ | Opaqueproof.PrivatePolymorphic _ -> assert false
+ in
+ let fc = Future.chain fc map in
+ match Future.peek_val fc with
+ | None -> [Later fc]
+ | Some c -> [Now c]
+ else []
in
- let fc = Future.chain fc map in
- begin match Future.peek_val fc with
- | None -> [Later fc]
- | Some c -> [Now c]
- end
- | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> []
+ senv, { cb with const_body = OpaqueDef o }, delayed_cst
+ | Undef _ | Def _ | Primitive _ as body ->
+ senv, { cb with const_body = body }, []
in
- let cb = map_constant (fun c -> Opaqueproof.create c) cb in
let senv = add_constant_aux ~in_section senv (kn, cb) in
add_constraints_list delayed_cst senv
in
@@ -985,6 +987,9 @@ let close_section senv =
that are going to be replayed. Those that are not forced are not readded
by {!add_constant_aux}. *)
let { rev_env = env; rev_univ = univ; rev_objlabels = objlabels } = revert in
+ (* Do not revert the opaque table, the discharged opaque constants are
+ referring to it. *)
+ let env = Environ.set_opaque_tables env (Environ.opaque_tables senv.env) in
let senv = { senv with env; revstruct; sections; univ; objlabels; } in
(* Second phase: replay the discharged section contents *)
let senv = add_constraints (Now cstrs) senv in
diff --git a/kernel/section.ml b/kernel/section.ml
index 4a9b222798..babd9fe7a1 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -146,19 +146,11 @@ let empty_segment = {
abstr_uctx = AUContext.empty;
}
-let extract_hyps sec vars hyps =
- (* FIXME: this code is fishy. It is supposed to check that declared section
- variables are an ordered subset of the ambient ones, but it doesn't check
- e.g. uniqueness of naming nor convertibility of the section data. *)
- let rec aux ids hyps = match ids, hyps with
- | id :: ids, decl :: hyps when Names.Id.equal id (NamedDecl.get_id decl) ->
- decl :: aux ids hyps
- | _ :: ids, hyps ->
- aux ids hyps
- | [], _ -> []
- in
- let ids = List.map NamedDecl.get_id @@ List.firstn sec.sec_context vars in
- aux ids hyps
+let extract_hyps sec vars used =
+ (* Keep the section-local segment of variables *)
+ let vars = List.firstn sec.sec_context vars in
+ (* Only keep the part that is used by the declaration *)
+ List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) used) vars
let section_segment_of_entry vars e hyps sections =
(* [vars] are the named hypotheses, [hyps] the subset that is declared by the
@@ -180,12 +172,14 @@ let section_segment_of_entry vars e hyps sections =
let segment_of_constant env con s =
let body = Environ.lookup_constant con env in
let vars = Environ.named_context env in
- section_segment_of_entry vars (SecDefinition con) body.Declarations.const_hyps s
+ let used = Context.Named.to_vars body.Declarations.const_hyps in
+ section_segment_of_entry vars (SecDefinition con) used s
let segment_of_inductive env mind s =
let mib = Environ.lookup_mind mind env in
let vars = Environ.named_context env in
- section_segment_of_entry vars (SecInductive mind) mib.Declarations.mind_hyps s
+ let used = Context.Named.to_vars mib.Declarations.mind_hyps in
+ section_segment_of_entry vars (SecInductive mind) used s
let instance_from_variable_context =
List.rev %> List.filter NamedDecl.is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b65e62ba30..f70b2960cf 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -221,9 +221,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
let build_constant_declaration env result =
let open Cooking in
let typ = result.cook_type in
- let check declared inferred =
- let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in
- let inferred_set, declared_set = mk_set inferred, mk_set declared in
+ let check declared_set inferred_set =
if not (Id.Set.subset inferred_set declared_set) then
let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in
let n = List.length l in
@@ -239,11 +237,6 @@ let build_constant_declaration env result =
str "Proof using " ++ declared_vars ++ fnl () ++
str "to" ++ fnl () ++
str "Proof using " ++ inferred_vars) in
- let sort l =
- List.filter (fun decl ->
- let id = NamedDecl.get_id decl in
- List.exists (NamedDecl.get_id %> Names.Id.equal id) l)
- (named_context env) in
(* We try to postpone the computation of used section variables *)
let hyps, def =
let context_ids = List.map NamedDecl.get_id (named_context env) in
@@ -252,7 +245,7 @@ let build_constant_declaration env result =
| None ->
if List.is_empty context_ids then
(* Empty section context: no need to check *)
- [], def
+ Id.Set.empty, def
else
(* No declared section vars, and non-empty section context:
we must look at the body NOW, if any *)
@@ -264,16 +257,19 @@ let build_constant_declaration env result =
(* Opaque definitions always come with their section variables *)
assert false
in
- keep_hyps env (Id.Set.union ids_typ ids_def), def
+ Environ.really_needed env (Id.Set.union ids_typ ids_def), def
| Some declared ->
+ let needed = Environ.really_needed env declared in
+ (* Transitive closure ensured by the upper layers *)
+ let () = assert (Id.Set.equal needed declared) in
(* We use the declared set and chain a check of correctness *)
- sort declared,
+ declared,
match def with
| Undef _ | Primitive _ as x -> x (* nothing to check *)
| Def cs as x ->
let ids_typ = global_vars_set env typ in
let ids_def = global_vars_set env (Mod_subst.force_constr cs) in
- let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
+ let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in
check declared inferred;
x
| OpaqueDef lc -> (* In this case we can postpone the check *)
@@ -281,12 +277,13 @@ let build_constant_declaration env result =
let kont c =
let ids_typ = global_vars_set env typ in
let ids_def = global_vars_set env c in
- let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
+ let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in
check declared inferred
in
OpaqueDef (iter kont lc)
in
let univs = result.cook_universes in
+ let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
let tps =
let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in
Option.map Cemitcodes.from_val res
@@ -317,7 +314,10 @@ let translate_recipe env _kn r =
let univs = result.cook_universes in
let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in
let tps = Option.map Cemitcodes.from_val res in
- { const_hyps = Option.get result.cook_context;
+ let hyps = Option.get result.cook_context in
+ (* Trust the set of section hypotheses generated by Cooking *)
+ let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
+ { const_hyps = hyps;
const_body = result.cook_body;
const_type = result.cook_type;
const_body_code = tps;
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 06:23:47 +0000