Merge PR #10817: Remove redundancy in section hypotheses of kernel entries.

Reviewed-by: SkySkimmer

1 files changed, 14 insertions, 14 deletions

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;