Merge PR #10427: Move internal flag

Reviewed-by: ejgallego

13 files changed, 35 insertions, 38 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..668026500d 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -27,12 +27,6 @@ open Cooking
 open Decls
 open Decl_kinds
 
-(** flag for internal message display *)
-type internal_flag =
-  | UserAutomaticRequest (* kernel action, a message is displayed *)
-  | InternalTacticRequest  (* kernel action, no message is displayed *)
-  | UserIndividualRequest   (* user action, a message is displayed *)
-
 type import_status = ImportDefaultBehavior | ImportNeedQualified
 
 (** Declaration of constants and parameters *)
@@ -233,7 +227,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 +235,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 +246,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..1f72fff30e 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -40,11 +40,6 @@ val declare_variable : variable -> variable_declaration -> Libobject.object_name
 
 type constant_declaration = Evd.side_effects constant_entry * logical_kind
 
-type internal_flag =
-  | UserAutomaticRequest
-  | InternalTacticRequest
-  | UserIndividualRequest
-
 (* Default definition entries, transparent with no secctx or proj information *)
 val definition_entry : ?fix_exn:Future.fix_exn ->
   ?opaque:bool -> ?inline:bool -> ?types:types ->
@@ -60,13 +55,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 8526bdd373..e01f3ab961 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -22,13 +22,18 @@ open Declarations
 open Constr
 open CErrors
 open Util
-open Declare
 open Decl_kinds
 open Pp
 
 (**********************************************************************)
 (* Registering schemes in the environment *)
 
+(** flag for internal message display *)
+type internal_flag =
+  | UserAutomaticRequest (* kernel action, a message is displayed *)
+  | InternalTacticRequest  (* kernel action, no message is displayed *)
+  | UserIndividualRequest   (* user action, a message is displayed *)
+
 type mutual_scheme_object_function =
   internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects
 type individual_scheme_object_function =
@@ -131,10 +136,10 @@ let define internal role id c poly univs =
     proof_entry_inline_code = false;
     proof_entry_feedback = None;
   } in
-  let kn, eff = declare_private_constant ~role ~internal id (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
     | InternalTacticRequest -> ()
-    | _-> definition_message id
+    | _-> Declare.definition_message id
   in
   kn, eff
 
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index 109fb64b2b..17e9c7ef42 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -10,7 +10,6 @@
 
 open Names
 open Constr
-open Declare
 
 (** This module provides support for registering inductive scheme builders,
    declaring schemes and generating schemes on demand *)
@@ -21,6 +20,11 @@ type mutual
 type individual
 type 'a scheme_kind
 
+type internal_flag =
+  | UserAutomaticRequest
+  | InternalTacticRequest
+  | UserIndividualRequest
+
 type mutual_scheme_object_function =
   internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects
 type individual_scheme_object_function =
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index d8f4b66d0e..e242b10d33 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -25,7 +25,6 @@ open Reductionops
 open Inductiveops
 open Tacmach.New
 open Clenv
-open Declare
 open Tacticals.New
 open Tactics
 open Decl_kinds
@@ -236,8 +235,8 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
 let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
   let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in
   let univs = Evd.univ_entry ~poly sigma in
-  let entry = definition_entry ~univs invProof in
-  let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
+  let entry = Declare.definition_entry ~univs invProof in
+  let _ = Declare.declare_constant name (Declare.DefinitionEntry entry, IsProof Lemma) in
   ()
 
 (* inv_op = Inv (derives de complete inv. lemma)
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 8b98408c5e..9b96fbf68a 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -676,9 +676,9 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
 let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
 
 let side_effect_of_mode = function
-  | Declare.UserAutomaticRequest -> false
-  | Declare.InternalTacticRequest -> true
-  | Declare.UserIndividualRequest -> false
+  | UserAutomaticRequest -> false
+  | InternalTacticRequest -> true
+  | UserIndividualRequest -> false
 
 let make_bl_scheme mode mind =
   let mib = Global.lookup_mind mind in
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)