Perform the opaque section variable inference outside of the kernel.

It is not the role of the kernel to decide to force the body of an entry
to infer the section variable it uses, but the one of the upper layers.
We make this explicit in the type of entries so as to enforce that this
inference is performed beforehand.

Also removes auxilliary file stuff that doesn't look like it belongs in
the kernel either.

4 files changed, 55 insertions, 30 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 2d29c3ee19..ca08ba485e 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -80,7 +80,7 @@ type section_def_entry = {
 type 'a opaque_entry = {
   opaque_entry_body   : 'a;
   (* List of section variables *)
-  opaque_entry_secctx : Constr.named_context option;
+  opaque_entry_secctx : Constr.named_context;
   (* State id on which the completion of type checking is reported *)
   opaque_entry_feedback : Stateid.t option;
   opaque_entry_type        : types;
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a0cc2974d9..7526508c4e 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -691,7 +691,7 @@ let constant_entry_of_side_effect eff =
   if Declareops.is_opaque cb then
   OpaqueEntry {
     opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
-    opaque_entry_secctx = None;
+    opaque_entry_secctx = cb.const_hyps;
     opaque_entry_feedback = None;
     opaque_entry_type = cb.const_type;
     opaque_entry_universes = univs;
@@ -699,7 +699,7 @@ let constant_entry_of_side_effect eff =
   else
   DefinitionEntry {
     const_entry_body = (p, Univ.ContextSet.empty);
-    const_entry_secctx = None;
+    const_entry_secctx = Some cb.const_hyps;
     const_entry_feedback = None;
     const_entry_type = Some cb.const_type;
     const_entry_universes = univs;
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 10221e18e9..b3c3dcbf45 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -151,7 +151,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         cook_universes = Monomorphic univs;
         cook_relevance = Sorts.relevance_of_sort tyj.utj_type;
         cook_inline = false;
-        cook_context = c.opaque_entry_secctx;
+        cook_context = Some c.opaque_entry_secctx;
       }
 
   (** Similar case for polymorphic entries. *)
@@ -188,7 +188,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         cook_universes = Polymorphic auctx;
         cook_relevance = Sorts.relevance_of_sort tj.utj_type;
         cook_inline = false;
-        cook_context = c.opaque_entry_secctx;
+        cook_context = Some c.opaque_entry_secctx;
       }
 
   (** Other definitions have to be processed immediately. *)
@@ -237,17 +237,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         cook_context = c.const_entry_secctx;
       }
 
-let record_aux env s_ty s_bo =
-  let in_ty = keep_hyps env s_ty in
-  let v =
-    String.concat " "
-      (CList.map_filter (fun decl ->
-          let id = NamedDecl.get_id decl in
-          if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None
-          else Some (Id.to_string id))
-        (keep_hyps env s_bo)) in
-  Aux_file.record_in_aux "context_used" v
-
 let build_constant_declaration env result =
   let open Cooking in
   let typ = result.cook_type in
@@ -279,24 +268,22 @@ let build_constant_declaration env result =
     let context_ids = List.map NamedDecl.get_id (named_context env) in
     let def = result.cook_body in
     match result.cook_context with
-    | None when not (List.is_empty context_ids) -> 
+    | None ->
+      if List.is_empty context_ids then
+        (* Empty section context: no need to check *)
+        [], def
+      else
         (* No declared section vars, and non-empty section context:
            we must look at the body NOW, if any *)
         let ids_typ = global_vars_set env typ in
         let ids_def = match def with
         | Undef _ | Primitive _ -> Id.Set.empty
         | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
-        | OpaqueDef lc ->
-            let (lc, _) = Future.force lc in
-            let vars = global_vars_set env lc in
-            if !Flags.record_aux_file then record_aux env ids_typ vars;
-            vars
+        | OpaqueDef _ ->
+          (* Opaque definitions always come with their section variables *)
+          assert false
         in
         keep_hyps env (Id.Set.union ids_typ ids_def), def
-    | None ->
-        if !Flags.record_aux_file then
-          record_aux env Id.Set.empty Id.Set.empty;
-        [], def (* Empty section context: no need to check *)
     | Some declared ->
         (* We use the declared set and chain a check of correctness *)
         sort declared,
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 668026500d..74196bb875 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -27,6 +27,8 @@ open Cooking
 open Decls
 open Decl_kinds
 
+module NamedDecl = Context.Named.Declaration
+
 type import_status = ImportDefaultBehavior | ImportNeedQualified
 
 (** Declaration of constants and parameters *)
@@ -144,6 +146,18 @@ let register_side_effect (c, role) =
   | None -> ()
   | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|]
 
+let record_aux env s_ty s_bo =
+  let open Environ in
+  let in_ty = keep_hyps env s_ty in
+  let v =
+    String.concat " "
+      (CList.map_filter (fun decl ->
+          let id = NamedDecl.get_id decl in
+          if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None
+          else Some (Id.to_string id))
+        (keep_hyps env s_bo)) in
+  Aux_file.record_in_aux "context_used" v
+
 let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
 let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body =
@@ -168,15 +182,39 @@ let cast_proof_entry e =
     const_entry_inline_code = e.proof_entry_inline_code;
   }
 
-let cast_opaque_proof_entry e =
+let cast_opaque_proof_entry (type a) (pure : a Safe_typing.effect_entry) (e : a Proof_global.proof_entry) =
   let open Proof_global in
   let typ = match e.proof_entry_type with
   | None -> assert false
   | Some typ -> typ
   in
+  let secctx = match e.proof_entry_secctx with
+  | None ->
+    let open Environ in
+    let env = Global.env () in
+    let hyp_typ, hyp_def =
+      if List.is_empty (Environ.named_context env) then
+        Id.Set.empty, Id.Set.empty
+      else
+        let ids_typ = global_vars_set env typ in
+        let pf, env = match pure with
+        | PureEntry ->
+          let (pf, _), () = Future.force e.proof_entry_body in
+          pf, env
+        | EffectEntry ->
+          let (pf, _), eff = Future.force e.proof_entry_body in
+          pf, Safe_typing.push_private_constants env eff
+        in
+        let vars = global_vars_set env pf in
+        ids_typ, vars
+    in
+    let () = if !Flags.record_aux_file then record_aux env hyp_typ hyp_def in
+    keep_hyps env (Id.Set.union hyp_typ hyp_def)
+  | Some hyps -> hyps
+  in
   {
     opaque_entry_body = e.proof_entry_body;
-    opaque_entry_secctx = e.proof_entry_secctx;
+    opaque_entry_secctx = secctx;
     opaque_entry_feedback = e.proof_entry_feedback;
     opaque_entry_type = typ;
     opaque_entry_universes = e.proof_entry_universes;
@@ -208,7 +246,7 @@ let define_constant ~side_effect id cd =
       let export = get_roles export eff in
       let de = { de with proof_entry_body = Future.from_val (body, ()) } in
       let cd = match de.proof_entry_opaque with
-      | true -> Entries.OpaqueEntry (cast_opaque_proof_entry de)
+      | true -> Entries.OpaqueEntry (cast_opaque_proof_entry PureEntry de)
       | false -> Entries.DefinitionEntry (cast_proof_entry de)
       in
       export, ConstantEntry (PureEntry, cd)
@@ -217,7 +255,7 @@ let define_constant ~side_effect id cd =
       let map (body, eff) = body, eff.Evd.seff_private in
       let body = Future.chain de.proof_entry_body map in
       let de = { de with proof_entry_body = body } in
-      let de = cast_opaque_proof_entry de in
+      let de = cast_opaque_proof_entry EffectEntry de in
       [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de)
     | ParameterEntry e ->
       [], ConstantEntry (PureEntry, Entries.ParameterEntry e)