Remove the internal_flag argument from Declare API.

It was never used actually.

10 files changed, 18 insertions, 18 deletions

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 9d928232c6..8acb29ba74 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1978,7 +1978,7 @@ let add_morphism_as_parameter atts m n : unit =
   let evd = Evd.from_env env in
   let uctx, instance = build_morphism_signature env evd m in
   let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
-  let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
+  let cst = Declare.declare_constant instance_id
       (Declare.ParameterEntry
          (None,(instance,uctx),None),
        Decl_kinds.IsAssumption Decl_kinds.Logical)
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
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 8addfa054e..35108744cd 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -337,7 +337,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst id
   let (_, ty_constr) = instance_constructor (k,u) subst in
   let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
   let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in
-  let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
+  let cst = Declare.declare_constant id
       (Declare.ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in
   Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
   instance_hook pri global imps (ConstRef cst)
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index e791118db2..e91d8b9d3e 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -280,7 +280,7 @@ let context ~poly l =
         let entry = Declare.definition_entry ~univs ~types:t b in
         (Declare.DefinitionEntry entry, IsAssumption Logical)
       in
-      let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
+      let cst = Declare.declare_constant id decl in
       let env = Global.env () in
       Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst);
       status
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index b393f33d5d..9559edbea0 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -100,8 +100,8 @@ let () =
 
 (* Util *)
 
-let define ~poly id internal sigma c t =
-  let f = declare_constant ~internal in
+let define ~poly id sigma c t =
+  let f = declare_constant in
   let univs = Evd.univ_entry ~poly sigma in
   let open Proof_global in
   let kn = f id
@@ -415,7 +415,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
     let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in
     let decltype = EConstr.to_constr sigma decltype in
     let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in
-    let cst = define ~poly fi UserIndividualRequest sigma proof_output (Some decltype) in
+    let cst = define ~poly fi sigma proof_output (Some decltype) in
     ConstRef cst :: lrecref
   in
   let _ = List.fold_right2 declare listdecl lrecnames [] in
@@ -544,7 +544,7 @@ let do_combined_scheme name schemes =
      some other polymorphism they can also manually define the
      combined scheme. *)
   let poly = Global.is_polymorphic (ConstRef (List.hd csts)) in
-  ignore (define ~poly name.v UserIndividualRequest sigma proof_output (Some typ));
+  ignore (define ~poly name.v sigma proof_output (Some typ));
   fixpoint_message None [name.v]
 
 (**********************************************************************)
diff --git a/vernac/record.ml b/vernac/record.ml
index 268c778674..cc4f02349d 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -353,7 +353,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags f
                     proof_entry_inline_code = false;
                     proof_entry_feedback = None } in
                   let k = (Declare.DefinitionEntry entry,IsDefinition kind) in
-		  let kn = declare_constant ~internal:InternalTacticRequest fid k in
+                  let kn = declare_constant fid k in
 		  let constr_fip =
 		    let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
 		      applist (mkConstU (kn,u),proj_args)