[ltac] Deprecate nameless fix/cofix.

LTAC's `fix` and `cofix` do require access to the proof object inside
the tactic monad when used without a name. This is a bit inconvenient
as we aim to make the handling of the proof object purely functional.

Alternatives have been discussed in #7196, and it seems that
deprecating the nameless forms may have the best cost/benefit ratio,
so opening this PR for discussion.

See also #6171.

14 files changed, 33 insertions, 22 deletions

diff --git a/CHANGES b/CHANGES
index 234d6c0db..994e8aede 100644
--- a/CHANGES
+++ b/CHANGES
@@ -27,6 +27,12 @@ Tools
   Coq was ignoring previous runs and the -async-proofs-delegation-threshold
   option did not have the expected behavior.
 
+Tactic language
+
+- The undocumented "nameless" forms `fix N`, `cofix N` have been
+  deprecated; please use `fix/cofix ident N` to explicitely name
+  hypothesis to be introduced.
+
 Changes from 8.7.2 to 8.8+beta1
 ===============================
 
diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex
index d0884be0d..01369b900 100644
--- a/doc/RecTutorial/RecTutorial.tex
+++ b/doc/RecTutorial/RecTutorial.tex
@@ -2978,7 +2978,7 @@ definition of \textsl{div\_aux}:
 
 \begin{alltt}
 Definition div_aux (x y:nat)(H: Acc lt x):nat.
- fix 3.
+ fix div_aux 3.
  intros.
  refine (if eq_nat_dec x 0 
          then 0 
@@ -3010,10 +3010,10 @@ Definition div x y := div_aux x y (lt_wf x).
 
 Let us explain the proof above. In the definition of \citecoq{div\_aux},
 what decreases is not $x$ but the \textsl{proof} of the accessibility
-of $x$. The tactic ``~\texttt{fix 3}~'' is used to indicate that the proof
+of $x$. The tactic ``~\texttt{fix div\_aux 3}~'' is used to indicate that the proof
 proceeds by structural induction on the third argument of the theorem
 --that is, on the accessibility proof. It also introduces a new
-hypothesis in the context, named as the current theorem, and with the
+hypothesis in the context, named ``~\texttt{div\_aux}~'', and with the
 same type as the goal. Then, the proof is refined with an incomplete
 proof term, containing a hole \texttt{\_}.  This hole corresponds to the proof
 of accessibility for $x-y$, and is filled up with the (smaller!)
diff --git a/doc/RecTutorial/RecTutorial.v b/doc/RecTutorial/RecTutorial.v
index 4b0ab3125..4a17e0818 100644
--- a/doc/RecTutorial/RecTutorial.v
+++ b/doc/RecTutorial/RecTutorial.v
@@ -922,7 +922,7 @@ Print minus_decrease.
 
 
 Definition div_aux (x y:nat)(H: Acc lt x):nat.
- fix 3.
+ fix div_aux 3.
  intros.
   refine (if eq_nat_dec x 0
          then 0
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d0ec3358a..6561a86c2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -557,8 +557,13 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl ->
   end
 end
 
+let warning_nameless_fix =
+    CWarnings.create ~name:"nameless-fix" ~category:"deprecated" Pp.(fun () ->
+        str "fix/cofix without a name are deprecated, please use the named version.")
+
 let fix ido n = match ido with
   | None ->
+    warning_nameless_fix ();
     Proofview.Goal.enter begin fun gl ->
       let name = Proof_global.get_current_proof_name () in
       let id = new_fresh_id Id.Set.empty name gl in
@@ -610,6 +615,7 @@ end
 
 let cofix ido = match ido with
   | None ->
+    warning_nameless_fix ();
     Proofview.Goal.enter begin fun gl ->
       let name = Proof_global.get_current_proof_name () in
       let id = new_fresh_id Id.Set.empty name gl in
diff --git a/test-suite/bugs/closed/2001.v b/test-suite/bugs/closed/2001.v
index d0b3bf173..652c65706 100644
--- a/test-suite/bugs/closed/2001.v
+++ b/test-suite/bugs/closed/2001.v
@@ -7,7 +7,7 @@ Inductive T : Set :=
 | v : T.
 
 Definition f (s:nat) (t:T) : nat.
-fix 2.
+fix f 2.
 intros s t.
 refine
   match t with
diff --git a/test-suite/bugs/closed/3320.v b/test-suite/bugs/closed/3320.v
index 0aac3c1b0..a5c243d8e 100644
--- a/test-suite/bugs/closed/3320.v
+++ b/test-suite/bugs/closed/3320.v
@@ -1,5 +1,5 @@
 Goal forall x : nat, True.
-  fix 1.
+  fix goal 1.
   assumption.
 Fail Qed.
 Undo.
diff --git a/test-suite/bugs/closed/3350.v b/test-suite/bugs/closed/3350.v
index c041c401f..c1ff292b3 100644
--- a/test-suite/bugs/closed/3350.v
+++ b/test-suite/bugs/closed/3350.v
@@ -55,7 +55,7 @@ Lemma lower_ind (P: forall n (p i:Fin.t (S n)), option (Fin.t n) -> Prop)
                 P (S n) (Fin.FS p) (Fin.FS i) None) :
   forall n (p i:Fin.t (S n)), P n p i (lower p i).
 Proof.
-  fix 2. intros n p.
+  fix lower_ind 2. intros n p.
   refine (match p as p1 in Fin.t (S n1)
                 return forall (i1:Fin.t (S n1)), P n1 p1 i1 (lower p1 i1)
           with
diff --git a/test-suite/success/ShowExtraction.v b/test-suite/success/ShowExtraction.v
index e34c240c5..a4a35003d 100644
--- a/test-suite/success/ShowExtraction.v
+++ b/test-suite/success/ShowExtraction.v
@@ -12,7 +12,7 @@ Fail Show Extraction.
 Lemma decListA : forall (xs ys : list A), {xs=ys}+{xs<>ys}.
 Proof.
 Show Extraction.
-fix 1.
+fix decListA 1.
 destruct xs as [|x xs], ys as [|y ys].
 Show Extraction.
 - now left.
diff --git a/test-suite/success/name_mangling.v b/test-suite/success/name_mangling.v
index 571dde880..e98241420 100644
--- a/test-suite/success/name_mangling.v
+++ b/test-suite/success/name_mangling.v
@@ -122,8 +122,7 @@ Lemma a : forall n, n = 0.
 Proof.
 fix a 1.
 Check a.
-fix 1.
-Fail Check a0.
+Fail fix a 1.
 Abort.
 
 (* Test stability of "induction" *)
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 42956c475..a5e457831 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -30,7 +30,7 @@ Lemma ind_0_1_SS :
     P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n.
 Proof.
   intros P H0 H1 H2.
-  fix 1.
+  fix ind_0_1_SS 1.
   destruct n as [|[|n]].
   - exact H0.
   - exact H1.
@@ -105,7 +105,7 @@ Hint Resolve double_S: arith.
 Lemma even_odd_double n :
   (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))).
 Proof.
-  revert n. fix 1. destruct n as [|[|n]].
+  revert n. fix even_odd_double 1. destruct n as [|[|n]].
   - (* n = 0 *)
     split; split; auto with arith. inversion 1.
   - (* n = 1 *)
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index baf119732..a1d0e9fcc 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -38,7 +38,7 @@ Hint Constructors odd: arith.
 
 Lemma even_equiv : forall n, even n <-> Nat.Even n.
 Proof.
- fix 1.
+ fix even_equiv 1.
  destruct n as [|[|n]]; simpl.
  - split; [now exists 0 | constructor].
  - split.
@@ -52,7 +52,7 @@ Qed.
 
 Lemma odd_equiv : forall n, odd n <-> Nat.Odd n.
 Proof.
- fix 1.
+ fix odd_equiv 1.
  destruct n as [|[|n]]; simpl.
  - split.
    + inversion_clear 1.
diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v
index 4e4938a99..bc58995fd 100644
--- a/theories/Arith/PeanoNat.v
+++ b/theories/Arith/PeanoNat.v
@@ -315,7 +315,7 @@ Import Private_Parity.
 
 Lemma even_spec : forall n, even n = true <-> Even n.
 Proof.
- fix 1.
+ fix even_spec 1.
   destruct n as [|[|n]]; simpl.
   - split; [ now exists 0 | trivial ].
   - split; [ discriminate | intro H; elim (Even_1 H) ].
@@ -325,7 +325,7 @@ Qed.
 Lemma odd_spec : forall n, odd n = true <-> Odd n.
 Proof.
  unfold odd.
- fix 1.
+ fix odd_spec 1.
   destruct n as [|[|n]]; simpl.
   - split; [ discriminate | intro H; elim (Odd_0 H) ].
   - split; [ now exists 0 | trivial ].
@@ -473,7 +473,7 @@ Notation "( x | y )" := (divide x y) (at level 0) : nat_scope.
 
 Lemma gcd_divide : forall a b, (gcd a b | a) /\ (gcd a b | b).
 Proof.
- fix 1.
+ fix gcd_divide 1.
  intros [|a] b; simpl.
  split.
   now exists 0.
@@ -502,7 +502,7 @@ Qed.
 
 Lemma gcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|gcd a b).
 Proof.
- fix 1.
+ fix gcd_greatest 1.
  intros [|a] b; simpl; auto.
  fold (b mod (S a)).
  intros c H H'. apply gcd_greatest; auto.
@@ -536,7 +536,7 @@ Qed.
 Lemma le_div2 n : div2 (S n) <= n.
 Proof.
  revert n.
- fix 1.
+ fix le_div2 1.
  destruct n; simpl; trivial. apply lt_succ_r.
  destruct n; [simpl|]; trivial. now constructor.
 Qed.
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 8d0896db7..000d895e1 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1655,7 +1655,7 @@ Qed.
 
 Lemma sqrtrem_spec p : SqrtSpec (sqrtrem p) p.
 Proof.
-revert p. fix 1.
+revert p. fix sqrtrem_spec 1.
  destruct p; try destruct p; try (constructor; easy);
   apply sqrtrem_step_spec; auto.
 Qed.
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index d9e5ad676..2ef162be4 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -148,10 +148,10 @@ Section defs.
     forall l1:list A, Sorted leA l1 ->
     forall l2:list A, Sorted leA l2 -> merge_lem l1 l2.
   Proof.
-    fix 1; intros; destruct l1.
+    fix merge 1; intros; destruct l1.
     apply merge_exist with l2; auto with datatypes.
     rename l1 into l.
-    revert l2 H0. fix 1. intros.
+    revert l2 H0. fix merge0 1. intros.
     destruct l2 as [|a0 l0]. 
     apply merge_exist with (a :: l); simpl; auto with datatypes. 
     induction (leA_dec a a0) as [Hle|Hle].