Dedicated type for opaque entries in the kernel.

Even more invariants can be enforced this way.

4 files changed, 33 insertions, 23 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 3f33df3f74..62aab7c391 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -77,6 +77,16 @@ type section_def_entry = {
   secdef_type : types option;
 }
 
+type 'a opaque_entry = {
+  opaque_entry_body   : 'a;
+  (* List of section variables *)
+  opaque_entry_secctx : Constr.named_context option;
+  (* State id on which the completion of type checking is reported *)
+  opaque_entry_feedback : Stateid.t option;
+  opaque_entry_type        : types option;
+  opaque_entry_universes   : universes_entry;
+  opaque_entry_inline_code : bool }
+
 type inline = int option (* inlining level, None for no inlining *)
 
 type parameter_entry = 
@@ -90,7 +100,7 @@ type primitive_entry = {
 
 type 'a constant_entry =
   | DefinitionEntry of constr Univ.in_universe_context_set definition_entry
-  | OpaqueEntry of 'a const_entry_body definition_entry
+  | OpaqueEntry of 'a const_entry_body opaque_entry
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ab58321ac7..5dac469a40 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -690,12 +690,12 @@ let constant_entry_of_side_effect eff =
     | _ -> assert false in
   if Declareops.is_opaque cb then
   OpaqueEntry {
-    const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
-    const_entry_secctx = None;
-    const_entry_feedback = None;
-    const_entry_type = Some cb.const_type;
-    const_entry_universes = univs;
-    const_entry_inline_code = cb.const_inline_code }
+    opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
+    opaque_entry_secctx = None;
+    opaque_entry_feedback = None;
+    opaque_entry_type = Some cb.const_type;
+    opaque_entry_universes = univs;
+    opaque_entry_inline_code = cb.const_inline_code }
   else
   DefinitionEntry {
     const_entry_body = (p, Univ.ContextSet.empty);
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 3b689953c8..2c31a237ce 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -115,11 +115,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
   (** Definition [c] is opaque (Qed), non polymorphic and with a specified type,
       so we delay the typing and hash consing of its body. *)
 
-  | OpaqueEntry ({ const_entry_type = typ;
-                       const_entry_universes = Monomorphic_entry univs; _ } as c) ->
+  | OpaqueEntry ({ opaque_entry_type = typ;
+                       opaque_entry_universes = Monomorphic_entry univs; _ } as c) ->
       let typ = match typ with None -> assert false | Some typ -> typ in
       let env = push_context_set ~strict:true univs env in
-      let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
+      let { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in
       let tyj = Typeops.infer_type env typ in
       let proofterm =
         Future.chain body begin fun ((body,uctx),side_eff) ->
@@ -151,16 +151,16 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         cook_type = tyj.utj_val;
         cook_universes = Monomorphic univs;
         cook_relevance = Sorts.relevance_of_sort tyj.utj_type;
-        cook_inline = c.const_entry_inline_code;
-        cook_context = c.const_entry_secctx;
+        cook_inline = c.opaque_entry_inline_code;
+        cook_context = c.opaque_entry_secctx;
       }
 
   (** Similar case for polymorphic entries. *)
 
-  | OpaqueEntry ({ const_entry_type = typ;
-                       const_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) ->
+  | OpaqueEntry ({ opaque_entry_type = typ;
+                       opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) ->
       let typ = match typ with None -> assert false | Some typ -> typ in
-      let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
+      let { opaque_entry_body = body; 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
@@ -189,8 +189,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         cook_type = typ;
         cook_universes = Polymorphic auctx;
         cook_relevance = Sorts.relevance_of_sort tj.utj_type;
-        cook_inline = c.const_entry_inline_code;
-        cook_context = c.const_entry_secctx;
+        cook_inline = c.opaque_entry_inline_code;
+        cook_context = c.opaque_entry_secctx;
       }
 
   (** Other definitions have to be processed immediately. *)
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 2178a7c54c..d4fdff76bf 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -175,12 +175,12 @@ let cast_proof_entry e =
 let cast_opaque_proof_entry e =
   let open Proof_global in
   {
-    const_entry_body = e.proof_entry_body;
-    const_entry_secctx = e.proof_entry_secctx;
-    const_entry_feedback = e.proof_entry_feedback;
-    const_entry_type = e.proof_entry_type;
-    const_entry_universes = e.proof_entry_universes;
-    const_entry_inline_code = e.proof_entry_inline_code;
+    opaque_entry_body = e.proof_entry_body;
+    opaque_entry_secctx = e.proof_entry_secctx;
+    opaque_entry_feedback = e.proof_entry_feedback;
+    opaque_entry_type = e.proof_entry_type;
+    opaque_entry_universes = e.proof_entry_universes;
+    opaque_entry_inline_code = e.proof_entry_inline_code;
   }
 
 let get_roles export eff =