Merge PR #10427: Move internal flag

Reviewed-by: ejgallego

5 files changed, 10 insertions, 10 deletions

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)