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

11 files changed, 14 insertions, 52 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 6438cf2571..9ee3c794d7 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -69,6 +69,9 @@ Vernacular commands
 
 - Removed the deprecated `Implicit Tactic` family of commands.
 
+- The `Automatic Introduction` option has been removed and is now the
+  default.
+
 Tools
 
 - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 741f9fe5b0..0b059f92ee 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -758,18 +758,6 @@ Controlling the effect of proof editing commands
    available hypotheses.
 
 
-.. flag:: Automatic Introduction
-
-   This option controls the way binders are handled
-   in assertion commands such as :n:`Theorem @ident {? @binders} : @term`. When the
-   option is on, which is the default, binders are automatically put in
-   the local context of the goal to prove.
-
-   When the option is off, binders are discharged on the statement to be
-   proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`)
-   has to be used to move the assumptions to the local context.
-
-
 .. flag:: Nested Proofs Allowed
 
    When turned on (it is off by default), this option enables support for nested
diff --git a/lib/flags.ml b/lib/flags.ml
index 582506f3a8..3aef5a7b2c 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -99,10 +99,6 @@ let verbosely f x = without_option quiet f x
 let if_silent f x = if !quiet then f x
 let if_verbose f x = if not !quiet then f x
 
-let auto_intros = ref true
-let make_auto_intros flag = auto_intros := flag
-let is_auto_intros () = !auto_intros
-
 let polymorphic_inductive_cumulativity = ref false
 let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b
 let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity
diff --git a/lib/flags.mli b/lib/flags.mli
index b667235678..e282d4ca8c 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -78,9 +78,6 @@ val if_silent : ('a -> unit) -> 'a -> unit
 val if_verbose : ('a -> unit) -> 'a -> unit
 
 (* Miscellaneus flags for vernac *)
-val make_auto_intros : bool -> unit
-val is_auto_intros : unit -> bool
-
 val program_mode : bool ref
 val is_program_mode : unit -> bool
 
diff --git a/test-suite/bugs/closed/bug_2001.v b/test-suite/bugs/closed/bug_2001.v
index 652c65706a..31c62b7b36 100644
--- a/test-suite/bugs/closed/bug_2001.v
+++ b/test-suite/bugs/closed/bug_2001.v
@@ -1,12 +1,10 @@
 (* Automatic computing of guard in "Theorem with"; check that guard is not
    computed when the user explicitly indicated it *)
 
-Unset Automatic Introduction.
-
 Inductive T : Set :=
 | v : T.
 
-Definition f (s:nat) (t:T) : nat.
+Definition f : forall (s:nat) (t:T), nat.
 fix f 2.
 intros s t.
 refine
diff --git a/test-suite/bugs/closed/bug_6661.v b/test-suite/bugs/closed/bug_6661.v
index e88a3704d8..28a9ffc7bd 100644
--- a/test-suite/bugs/closed/bug_6661.v
+++ b/test-suite/bugs/closed/bug_6661.v
@@ -53,8 +53,6 @@ Definition foo (X:Type) (xy : @total2 X (λ _, X)) : X.
   exact x.
 Defined.
 
-Unset Automatic Introduction.
-
 Definition idfun (T : UU) := λ t:T, t.
 
 Definition pathscomp0 {X : UU} {a b c : X} (e1 : a = b) (e2 : b = c) : a = c.
diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v
index efb32ef6f7..81c9763ccd 100644
--- a/test-suite/success/Fixpoint.v
+++ b/test-suite/success/Fixpoint.v
@@ -50,8 +50,6 @@ End folding.
 
 (* Check definition by tactics *)
 
-Set Automatic Introduction.
-
 Inductive even : nat -> Type :=
   | even_O : even 0
   | even_S : forall n, odd n -> even (S n)
diff --git a/test-suite/success/autointros.v b/test-suite/success/autointros.v
index 0a0812711c..1140a537fc 100644
--- a/test-suite/success/autointros.v
+++ b/test-suite/success/autointros.v
@@ -1,5 +1,3 @@
-Set Automatic Introduction.
-
 Inductive even : nat -> Prop :=
 | even_0 : even 0
 | even_odd : forall n, odd n -> even (S n)
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"];