Remove the export_seff flag from Declare API.

It was always the negation of the opacity flag.

3 files changed, 8 insertions, 9 deletions

diff --git a/tactics/declare.ml b/tactics/declare.ml
index fdb8155038..ca5d265733 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -193,7 +193,7 @@ let get_roles export eff =
   in
   List.map map export
 
-let define_constant ~side_effect ?(export_seff=false) id cd =
+let define_constant ~side_effect id cd =
   let open Proof_global in
   (* Logically define the constant and its subproofs, no libobject tampering *)
   let is_poly de = match de.proof_entry_universes with
@@ -204,7 +204,6 @@ let define_constant ~side_effect ?(export_seff=false) id cd =
   let export, decl = (* We deal with side effects *)
     match cd with
     | DefinitionEntry de when
-        export_seff ||
         not de.proof_entry_opaque ||
         is_poly de ->
       (* This globally defines the side-effects in the environment. *)
@@ -232,9 +231,9 @@ let define_constant ~side_effect ?(export_seff=false) id cd =
   let kn, eff = Global.add_constant ~side_effect ~in_section id decl in
   kn, eff, export
 
-let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefaultBehavior) id ?(export_seff=false) (cd, kind) =
+let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) =
   let () = check_exists id in
-  let kn, (), export = define_constant ~side_effect:PureEntry ~export_seff id cd in
+  let kn, (), export = define_constant ~side_effect:PureEntry id cd in
   (* Register the libobjects attached to the constants and its subproofs *)
   let () = List.iter register_side_effect export in
   let () = register_constant kn kind local in
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 692eca8dde..0a2332748c 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -58,7 +58,7 @@ val definition_entry : ?fix_exn:Future.fix_exn ->
   internal specify if the constant has been created by the kernel or by the
   user, and in the former case, if its errors should be silent *)
 val declare_constant :
- ?internal:internal_flag -> ?local:import_status -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t
+ ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t
 
 val declare_private_constant :
   ?role:Evd.side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects
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