Remove the internal_flag argument from Declare API.

It was never used actually.

5 files changed, 10 insertions, 10 deletions

diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 465f736032..662a2fc22c 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -158,7 +158,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
     (* do not compute the implicit arguments, it may be costly *)
     let () = Impargs.make_implicit_args false in
     (* ppedrot: seems legit to have abstracted subproofs as local*)
-    Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:Declare.ImportNeedQualified name decl
+    Declare.declare_private_constant ~local:Declare.ImportNeedQualified name decl
   in
   let cst, eff = Impargs.with_implicit_protection cst () in
   let inst = match const.Proof_global.proof_entry_universes with
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 4a4e2cf60a..27c2d089f6 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -233,7 +233,7 @@ let define_constant ~side_effect 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 (cd, kind) =
+let declare_constant ?(local = ImportDefaultBehavior) id (cd, kind) =
   let () = check_exists id in
   let kn, (), export = define_constant ~side_effect:PureEntry id cd in
   (* Register the libobjects attached to the constants and its subproofs *)
@@ -241,7 +241,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefault
   let () = register_constant kn kind local in
   kn
 
-let declare_private_constant ?role ?(internal=UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) =
+let declare_private_constant ?role ?(local = ImportDefaultBehavior) id (cd, kind) =
   let kn, eff, export = define_constant ~side_effect:EffectEntry id cd in
   let () = assert (List.is_empty export) in
   let () = register_constant kn kind local in
@@ -252,13 +252,13 @@ let declare_private_constant ?role ?(internal=UserIndividualRequest) ?(local = I
   let eff = { Evd.seff_private = eff; Evd.seff_roles; } in
   kn, eff
 
-let declare_definition ?(internal=UserIndividualRequest)
+let declare_definition
   ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = ImportDefaultBehavior)
   id ?types (body,univs) =
   let cb =
     definition_entry ?types ~univs ~opaque body
   in
-    declare_constant ~internal ~local id
+    declare_constant ~local id
       (DefinitionEntry cb, Decl_kinds.IsDefinition kind)
 
 (** Declaration of section variables and local definitions *)
diff --git a/tactics/declare.mli b/tactics/declare.mli
index d87c096119..495f66c745 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -60,13 +60,13 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified
   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 -> constant_declaration -> Constant.t
+ ?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
+  ?role:Evd.side_effect_role -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects
 
 val declare_definition :
-  ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
+  ?opaque:bool -> ?kind:definition_object_kind ->
   ?local:import_status -> Id.t -> ?types:constr ->
   constr Entries.in_universes_entry -> Constant.t
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 014e54158d..3a3a6b94dc 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1320,7 +1320,7 @@ let project_hint ~poly pri l2r r =
   in
   let ctx = Evd.univ_entry ~poly sigma in
   let c = EConstr.to_constr sigma c in
-  let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
+  let c = Declare.declare_definition id (c,ctx) in
   let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
     (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c))
 
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 23fa1a312c..d5e88791a6 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -130,7 +130,7 @@ let define internal role id c poly univs =
     proof_entry_inline_code = false;
     proof_entry_feedback = None;
   } in
-  let kn, eff = Declare.declare_private_constant ~role ~internal id (Declare.DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
+  let kn, eff = Declare.declare_private_constant ~role id (Declare.DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
   let () = match internal with
     | Declare.InternalTacticRequest -> ()
     | _-> Declare.definition_message id