Remove redundancy in section hypotheses of kernel entries.

We only do it for entries and not declarations because the upper layers
rely on the kernel being able to quickly tell that a definition is improperly
used inside a section. Typically, tactics can mess with the named context
and thus make the use of section definitions illegal. This cannot happen in
the kernel but we cannot remove it due to the code dependency.

Probably fixing a soundness bug reachable via ML code only. We were doing
fancy things w.r.t. computation of the transitive closure of the the variables,
in particular lack of proper sanitization of the kernel input.

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;