Merge PR #9001: [options] Remove deprecated option automatic introduction.

3 files changed, 10 insertions, 24 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index b0dba2485a..95e46b252b 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -188,8 +188,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
             ]
           in
           ignore (Pfedit.by init_refine)
-        else if Flags.is_auto_intros () then
-          ignore (Pfedit.by (Tactics.auto_intros_tac ids));
+        else ignore (Pfedit.by (Tactics.auto_intros_tac ids));
         (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ()
 
 let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 437eee3413..4e847a5590 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -373,22 +373,17 @@ let start_proof_with_initialization kind sigma decl recguard thms snl hook =
   let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in
   let init_tac,guard = match recguard with
   | Some (finite,guard,init_tac) ->
-      let rec_tac = rec_tac_initializer finite guard thms snl in
-      Some (match init_tac with
-        | None -> 
-            if Flags.is_auto_intros () then 
-              Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms)
-            else
-              rec_tac
+    let rec_tac = rec_tac_initializer finite guard thms snl in
+    Some (match init_tac with
+        | None ->
+          Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms)
         | Some tacl ->
-            Tacticals.New.tclTHENS rec_tac
-            (if Flags.is_auto_intros () then
-              List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms
-            else
-              tacl)),guard
+          Tacticals.New.tclTHENS rec_tac
+            List.(map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms)
+      ),guard
   | None ->
-      let () = match thms with [_] -> () | _ -> assert false in
-      (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
+    let () = match thms with [_] -> () | _ -> assert false in
+    Some (intro_tac (List.hd thms)), [] in
   match thms with
   | [] -> anomaly (Pp.str "No proof to start.")
   | (id,(t,(_,imps)))::other_thms ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 7a76fb9560..08aee9533f 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1453,14 +1453,6 @@ let _ =
 
 let _ =
   declare_bool_option
-    { optdepr  = true; (* remove in 8.8 *)
-      optname  = "automatic introduction of variables";
-      optkey   = ["Automatic";"Introduction"];
-      optread  = Flags.is_auto_intros;
-      optwrite = Flags.make_auto_intros }
-
-let _ =
-  declare_bool_option
     { optdepr  = false;
       optname  = "coercion printing";
       optkey   = ["Printing";"Coercions"];