diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 11 |
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 -> |