diff options
| author | Pierre-Marie Pédrot | 2019-06-24 16:17:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-24 16:27:46 +0200 |
| commit | 34ef770191b692340bcf448ecc6edbaf8abe8c1e (patch) | |
| tree | 58097543ff3e713a869a51b09ab2f2e885e174d3 /vernac | |
| parent | d2abcce128c0ba9f62fed66a1bca9c294be0c9c0 (diff) | |
Remove the export_seff flag from Declare API.
It was always the negation of the opacity flag.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/lemmas.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 73403d9417..c2de83c1bb 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -497,9 +497,9 @@ let finish_proved opaque idopt po hook compute_guard = let open Proof_global in match po with | { id; entries=[const]; persistence=locality,poly,kind; universes } -> - let is_opaque, export_seff = match opaque with - | Transparent -> false, true - | Opaque -> true, false + let is_opaque = match opaque with + | Transparent -> false + | Opaque -> true in assert (is_opaque == const.proof_entry_opaque); let id = match idopt with @@ -520,7 +520,7 @@ let finish_proved opaque idopt po hook compute_guard = VarRef id | Global local -> let kn = - declare_constant ~export_seff id ~local (DefinitionEntry const, k) in + declare_constant id ~local (DefinitionEntry const, k) in let () = if should_suggest then Proof_using.suggest_constant (Global.env ()) kn in |