Cleaning up the previous code by ensuring statically invariants on opaque proofs.

We return the typing context directly instead of hiding it into the opaque
data, and we take advantage of this to remove a few assertions known to hold
statically.

1 files changed, 42 insertions, 42 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 1e0db8026f..f85b3db413 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -64,7 +64,7 @@ type typing_context =
 | MonoTyCtx of Environ.env * unsafe_type_judgment * Univ.ContextSet.t * Id.Set.t * Stateid.t option
 | PolyTyCtx of Environ.env * unsafe_type_judgment * Univ.universe_level_subst * Univ.AUContext.t * Id.Set.t * Stateid.t option
 
-let infer_declaration (type a) env (dcl : a constant_entry) =
+let infer_declaration env (dcl : constant_entry) =
   match dcl with
     | ParameterEntry (ctx,(t,uctx),nl) ->
       let env = match uctx with
@@ -112,47 +112,6 @@ let infer_declaration (type a) env (dcl : a constant_entry) =
         cook_relevance = Sorts.Relevant;
       }
 
-  (** Definition [c] is opaque (Qed), non polymorphic and with a specified type,
-      so we delay the typing and hash consing of its body. *)
-
-  | OpaqueEntry ({ opaque_entry_type = typ;
-                       opaque_entry_universes = Monomorphic_entry univs; _ } as c) ->
-      let env = push_context_set ~strict:true univs env in
-      let { opaque_entry_feedback = feedback_id; _ } = c in
-      let tyj = Typeops.infer_type env typ in
-      let context = MonoTyCtx (env, tyj, univs, c.opaque_entry_secctx, feedback_id) in
-      let def = OpaqueDef context in
-      {
-        Cooking.cook_body = def;
-        cook_type = tyj.utj_val;
-        cook_universes = Monomorphic univs;
-        cook_relevance = Sorts.relevance_of_sort tyj.utj_type;
-        cook_inline = false;
-        cook_context = Some c.opaque_entry_secctx;
-      }
-
-  (** Similar case for polymorphic entries. *)
-
-  | OpaqueEntry ({ opaque_entry_type = typ;
-                       opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) ->
-      let { opaque_entry_feedback = feedback_id; _ } = c in
-      let env = push_context ~strict:false uctx env in
-      let tj = Typeops.infer_type env typ in
-      let sbst, auctx = Univ.abstract_universes nas uctx in
-      let usubst = Univ.make_instance_subst sbst in
-      let context = PolyTyCtx (env, tj, usubst, auctx, c.opaque_entry_secctx, feedback_id) in
-      let def = OpaqueDef context in
-      let typ = Vars.subst_univs_level_constr usubst tj.utj_val in
-      {
-        Cooking.cook_body = def;
-        cook_type = typ;
-        cook_universes = Polymorphic auctx;
-        cook_relevance = Sorts.relevance_of_sort tj.utj_type;
-        cook_inline = false;
-        cook_context = Some c.opaque_entry_secctx;
-      }
-
-  (** Other definitions have to be processed immediately. *)
   | DefinitionEntry c ->
       let { const_entry_type = typ; _ } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
@@ -189,6 +148,43 @@ let infer_declaration (type a) env (dcl : a constant_entry) =
         cook_context = c.const_entry_secctx;
       }
 
+(** Definition is opaque (Qed), so we delay the typing of its body. *)
+let infer_opaque env = function
+  | ({ opaque_entry_type = typ;
+                       opaque_entry_universes = Monomorphic_entry univs; _ } as c) ->
+      let env = push_context_set ~strict:true univs env in
+      let { opaque_entry_feedback = feedback_id; _ } = c in
+      let tyj = Typeops.infer_type env typ in
+      let context = MonoTyCtx (env, tyj, univs, c.opaque_entry_secctx, feedback_id) in
+      let def = OpaqueDef () in
+      {
+        Cooking.cook_body = def;
+        cook_type = tyj.utj_val;
+        cook_universes = Monomorphic univs;
+        cook_relevance = Sorts.relevance_of_sort tyj.utj_type;
+        cook_inline = false;
+        cook_context = Some c.opaque_entry_secctx;
+      }, context
+
+  | ({ opaque_entry_type = typ;
+                       opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) ->
+      let { opaque_entry_feedback = feedback_id; _ } = c in
+      let env = push_context ~strict:false uctx env in
+      let tj = Typeops.infer_type env typ in
+      let sbst, auctx = Univ.abstract_universes nas uctx in
+      let usubst = Univ.make_instance_subst sbst in
+      let context = PolyTyCtx (env, tj, usubst, auctx, c.opaque_entry_secctx, feedback_id) in
+      let def = OpaqueDef () in
+      let typ = Vars.subst_univs_level_constr usubst tj.utj_val in
+      {
+        Cooking.cook_body = def;
+        cook_type = typ;
+        cook_universes = Polymorphic auctx;
+        cook_relevance = Sorts.relevance_of_sort tj.utj_type;
+        cook_inline = false;
+        cook_context = Some c.opaque_entry_secctx;
+      }, context
+
 let check_section_variables env declared_set typ body =
   let ids_typ = global_vars_set env typ in
   let ids_def = global_vars_set env body in
@@ -297,6 +293,10 @@ let translate_constant env _kn ce =
   build_constant_declaration env
     (infer_declaration env ce)
 
+let translate_opaque env _kn ce =
+  let def, ctx = infer_opaque env ce in
+  build_constant_declaration env def, ctx
+
 let translate_local_assum env t =
   let j = Typeops.infer env t in
   let t = Typeops.assumption_of_judgment env j in