aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES6
-rw-r--r--doc/RecTutorial/RecTutorial.tex6
-rw-r--r--doc/RecTutorial/RecTutorial.v2
-rw-r--r--tactics/tactics.ml6
-rw-r--r--test-suite/bugs/closed/2001.v2
-rw-r--r--test-suite/bugs/closed/3320.v2
-rw-r--r--test-suite/bugs/closed/3350.v2
-rw-r--r--test-suite/success/ShowExtraction.v2
-rw-r--r--test-suite/success/name_mangling.v3
-rw-r--r--theories/Arith/Div2.v4
-rw-r--r--theories/Arith/Even.v4
-rw-r--r--theories/Arith/PeanoNat.v10
-rw-r--r--theories/PArith/BinPos.v2
-rw-r--r--theories/Sorting/Heap.v4
14 files changed, 33 insertions, 22 deletions
diff --git a/CHANGES b/CHANGES
index 9f4c71a56..06a9bba7d 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 efb46e7d9..aae4bc088 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].
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-20 05:35:25 +0000