From 2243c25c79ab19876ad74452c9cecc7dcc88c67c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 9 Apr 2018 01:33:31 +0200
Subject: [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.
---
 theories/Arith/Div2.v     |  4 ++--
 theories/Arith/Even.v     |  4 ++--
 theories/Arith/PeanoNat.v | 10 +++++-----
 theories/PArith/BinPos.v  |  2 +-
 theories/Sorting/Heap.v   |  4 ++--
 5 files changed, 12 insertions(+), 12 deletions(-)

(limited to 'theories')

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].
-- 
cgit v1.2.3