Simplify internal flags in scheme declarations.

2 files changed, 10 insertions, 12 deletions

diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 9c94f3c319..3c0cf1a3c0 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -82,10 +82,9 @@ let is_visible_name id =
   with Not_found -> false
 
 let compute_name internal id =
-  match internal with
-  | UserAutomaticRequest | UserIndividualRequest -> id
-  | InternalTacticRequest ->
-      Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
+  if internal then
+    Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
+  else id
 
 let define internal role id c poly univs =
   let id = compute_name internal id in
@@ -94,10 +93,7 @@ let define internal role id c poly univs =
   let univs = UState.univ_entry ~poly ctx in
   let entry = Declare.pure_definition_entry ~univs c in
   let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id entry in
-  let () = match internal with
-    | InternalTacticRequest -> ()
-    | _-> Declare.definition_message id
-  in
+  let () = if internal then () else Declare.definition_message id in
   kn, eff
 
 let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
@@ -107,7 +103,8 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
     | Some id -> id
     | None -> add_suffix mib.mind_packets.(i).mind_typename suff in
   let role = Evd.Schema (ind, kind) in
-  let const, neff = define mode role id c (Declareops.inductive_is_polymorphic mib) ctx in
+  let internal = mode == InternalTacticRequest in
+  let const, neff = define internal role id c (Declareops.inductive_is_polymorphic mib) ctx in
   DeclareScheme.declare_scheme kind [|ind,const|];
   const, Evd.concat_side_effects neff eff
 
@@ -125,7 +122,8 @@ let define_mutual_scheme_base kind suff f mode names mind =
       with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
   let fold i effs id cl =
     let role = Evd.Schema ((mind, i), kind)in
-    let cst, neff = define mode role id cl (Declareops.inductive_is_polymorphic mib) ctx in
+    let internal = mode == InternalTacticRequest in
+    let cst, neff = define internal role id cl (Declareops.inductive_is_polymorphic mib) ctx in
     (Evd.concat_side_effects neff effs, cst)
   in
   let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 310ea62a1d..f954915cf8 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -430,7 +430,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
   end
 
 (* used in the bool -> leb side *)
-let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
+let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
   let open EConstr in
   let avoid = Array.of_list aavoid in
   let do_arg sigma hd v offset =
@@ -658,7 +658,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                               if GlobRef.equal (GlobRef.IndRef indeq) Coqlib.(lib_ref "core.eq.type")
                               then
                                 Tacticals.New.tclTHEN
-                                  (do_replace_bl mode bl_scheme_key ind
+                                  (do_replace_bl bl_scheme_key ind
                                      (!avoid)
                                      nparrec (ca.(2))
                                      (ca.(1)))