Do not perform the section variable check on global recipes.

By construction, we know that Cooking is returning the right set of
used variables. This set has been checked already once at the time
when the definition was performed inside the section.

4 files changed, 19 insertions, 22 deletions

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 423a416ca4..18c1bcc0f8 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -77,11 +77,6 @@ let subst_opaque sub = function
   | Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
   | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.")
 
-let iter_direct_opaque f = function
-  | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
-  | Direct (d,cu) ->
-      Direct (d,Future.chain cu (fun (c, u) -> f c; c, u))
-
 let discharge_direct_opaque ~cook_constr ci = function
   | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
   | Direct (d,cu) ->
@@ -100,10 +95,6 @@ let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
         let fp = snd (Int.Map.find i prfs) in
         join except fp
 
-let force_direct = function
-| Direct (_, cu) -> Future.force cu
-| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
-
 let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) ->
       fst(Future.force cu)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 8b6e8a1c8f..4e8956af06 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -39,12 +39,10 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
     indirect opaque accessor configured below. *)
 val force_proof : opaquetab -> opaque -> constr
 val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
-val force_direct : opaque -> (constr * Univ.ContextSet.t)
 val get_constraints :
   opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
 
 val subst_opaque : substitution -> opaque -> opaque
-val iter_direct_opaque : (constr -> unit) -> opaque -> opaque
 
 type work_list = (Univ.Instance.t * Id.t array) Cmap.t * 
   (Univ.Instance.t * Id.t array) Mindmap.t
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 9e33b431fc..74c6189a65 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -232,7 +232,7 @@ let record_aux env s_ty s_bo =
         (keep_hyps env s_bo)) in
   Aux_file.record_in_aux "context_used" v
 
-let build_constant_declaration ~force ~iter env result =
+let build_constant_declaration env result =
   let open Cooking in
   let typ = result.cook_type in
   let check declared inferred =
@@ -271,7 +271,7 @@ let build_constant_declaration ~force ~iter env result =
         | Undef _ | Primitive _ -> Id.Set.empty
         | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
         | OpaqueDef lc ->
-            let (lc, _) = force lc in
+            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
@@ -293,6 +293,7 @@ let build_constant_declaration ~force ~iter env result =
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
+          let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in
           let kont c =
             let ids_typ = global_vars_set env typ in
             let ids_def = global_vars_set env c in
@@ -319,9 +320,7 @@ let build_constant_declaration ~force ~iter env result =
 (*s Global and local constant declaration. *)
 
 let translate_constant mb env _kn ce =
-  let force cu = Future.force cu in
-  let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in
-  build_constant_declaration ~force ~iter env
+  build_constant_declaration env
     (infer_declaration ~trust:mb env ce)
 
 let translate_local_assum env t =
@@ -330,9 +329,20 @@ let translate_local_assum env t =
     j.uj_val, t
 
 let translate_recipe ~hcons env _kn r =
-  let force o = Opaqueproof.force_direct o in
-  let iter k o = Opaqueproof.iter_direct_opaque k o in
-  build_constant_declaration ~force ~iter env (Cooking.cook_constant ~hcons r)
+  let open Cooking in
+  let result = Cooking.cook_constant ~hcons r in
+  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;
+    const_body = result.cook_body;
+    const_type = result.cook_type;
+    const_body_code = tps;
+    const_universes = univs;
+    const_private_poly_univs = result.cook_private_univs;
+    const_relevance = result.cook_relevance;
+    const_inline_code = result.cook_inline;
+    const_typing_flags = Environ.typing_flags env }
 
 let translate_local_def env _id centry =
   let open Cooking in
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index a046d26ea9..592a97e132 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -43,6 +43,4 @@ val infer_declaration : trust:'a trust -> env ->
   'a constant_entry -> Opaqueproof.proofterm Cooking.result
 
 val build_constant_declaration :
-  force:('a -> constr * 'b) ->
-  iter:((constr -> unit) -> 'a -> 'a) ->
-  env -> 'a Cooking.result -> 'a constant_body
+  env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body