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

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

1 files changed, 7 insertions, 4 deletions

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 ->