Enforce that opaque entries carry their type.

4 files changed, 7 insertions, 5 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 62aab7c391..6016510189 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -83,7 +83,7 @@ type 'a opaque_entry = {
   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_type        : types;
   opaque_entry_universes   : universes_entry;
   opaque_entry_inline_code : bool }
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 5dac469a40..6cb7a22a15 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -693,7 +693,7 @@ let constant_entry_of_side_effect eff =
     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_type = cb.const_type;
     opaque_entry_universes = univs;
     opaque_entry_inline_code = cb.const_inline_code }
   else
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 2c31a237ce..86d79ba044 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -117,7 +117,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
 
   | 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 { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in
       let tyj = Typeops.infer_type env typ in
@@ -159,7 +158,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
 
   | 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 { 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
diff --git a/tactics/declare.ml b/tactics/declare.ml
index d4fdff76bf..3840aa6be1 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -174,11 +174,15 @@ let cast_proof_entry e =
 
 let cast_opaque_proof_entry e =
   let open Proof_global in
+  let typ = match e.proof_entry_type with
+  | None -> assert false
+  | Some typ -> typ
+  in
   {
     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_type = typ;
     opaque_entry_universes = e.proof_entry_universes;
     opaque_entry_inline_code = e.proof_entry_inline_code;
   }