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, 9 insertions, 15 deletions

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