Take advantage of the change of entry representation to split opacity status.

Mere isomorphism for now, but will allow more invariants ultimately.

4 files changed, 22 insertions, 14 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index de1ce609fd..1a25337512 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -68,7 +68,6 @@ type 'a definition_entry = {
   const_entry_feedback : Stateid.t option;
   const_entry_type        : types option;
   const_entry_universes   : universes_entry;
-  const_entry_opaque      : bool;
   const_entry_inline_code : bool }
 
 type section_def_entry = {
@@ -91,6 +90,7 @@ type primitive_entry = {
 
 type 'a constant_entry =
   | DefinitionEntry of 'a definition_entry
+  | OpaqueEntry of 'a definition_entry
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a980d22e42..c99edccda7 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -688,13 +688,21 @@ let constant_entry_of_side_effect eff =
     | OpaqueDef b -> b
     | Def b -> Mod_subst.force_constr b
     | _ -> 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 }
+  else
   DefinitionEntry {
     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_opaque = Declareops.is_opaque cb;
     const_entry_inline_code = cb.const_inline_code }
 
 let export_eff eff =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 165feca1b6..e28849c953 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -115,9 +115,9 @@ 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. *)
 
-  | DefinitionEntry ({ const_entry_type = Some typ;
-                       const_entry_opaque = true;
+  | OpaqueEntry ({ const_entry_type = typ;
                        const_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 tyj = Typeops.infer_type env typ in
@@ -155,12 +155,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         cook_context = c.const_entry_secctx;
       }
 
-  (** Similar case for polymorphic entries. TODO: also delay type-checking of
-      the body. *)
+  (** Similar case for polymorphic entries. *)
 
-  | DefinitionEntry ({ const_entry_type = Some typ;
-                       const_entry_opaque = true;
+  | OpaqueEntry ({ const_entry_type = typ;
                        const_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 env = push_context ~strict:false uctx env in
       let tj = Typeops.infer_type env typ in
@@ -200,7 +199,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
       (* Opaque constants must be provided with a non-empty const_entry_type,
          and thus should have been treated above. *)
-      let () = assert (not c.const_entry_opaque) in
       let body, ctx = match trust with
       | Pure ->
         let (body, ctx), () = Future.join body in
@@ -375,7 +373,6 @@ let translate_local_def env _id centry =
     const_entry_feedback = centry.secdef_feedback;
     const_entry_type = centry.secdef_type;
     const_entry_universes = Monomorphic_entry Univ.ContextSet.empty;
-    const_entry_opaque = false;
     const_entry_inline_code = false;
   } in
   let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 81663b9b99..b35d4a5d66 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -168,7 +168,6 @@ let cast_proof_entry e =
     const_entry_feedback = e.proof_entry_feedback;
     const_entry_type = e.proof_entry_type;
     const_entry_universes = e.proof_entry_universes;
-    const_entry_opaque = e.proof_entry_opaque;
     const_entry_inline_code = e.proof_entry_inline_code;
   }
 
@@ -198,14 +197,18 @@ let define_constant ~side_effect ?(export_seff=false) id cd =
       let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in
       let export = get_roles export eff in
       let de = { de with proof_entry_body = Future.from_val (body, ()) } in
-      let de = cast_proof_entry de in
-      export, ConstantEntry (PureEntry, Entries.DefinitionEntry de)
+      let cd = match de.proof_entry_opaque with
+      | true -> Entries.OpaqueEntry (cast_proof_entry de)
+      | false -> Entries.DefinitionEntry (cast_proof_entry de)
+      in
+      export, ConstantEntry (PureEntry, cd)
     | DefinitionEntry de ->
+      let () = assert (de.proof_entry_opaque) in
       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_proof_entry de in
-      [], ConstantEntry (EffectEntry, Entries.DefinitionEntry de)
+      [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de)
     | ParameterEntry e ->
       [], ConstantEntry (PureEntry, Entries.ParameterEntry e)
     | PrimitiveEntry e ->