[tactics] Remove anonymous fix/cofix form.

We remove the `fix N / cofix N` forms from the tactic language. This
way, these tactics don't depend anymore on the proof context, in
particular on the proof name, which seems like a fragile practice.

Apart from the concerns wrt maintenability of proof scripts, this also
helps making the "proof state" functional; as we don't have to
propagate the proof name to the tactic layer.

1 files changed, 19 insertions, 17 deletions

diff --git a/CHANGES b/CHANGES
index aea7ec2f6..ac4f3fa06 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,6 +7,22 @@ Tactics
   Use with Set Default Goal Selector to force focusing before tactics
   are called.
 
+- The undocumented "nameless" forms `fix N`, `cofix` that were
+  deprecated in 8.8 have been removed from LTAC's syntax; please use
+  `fix ident N/cofix ident` to explicitely name the (co)fixpoint
+  hypothesis to be introduced.
+
+- Introduction tactics "intro"/"intros" on a goal which is an
+  existential variable now force a refinement of the goal into a
+  dependent product rather than failing.
+
+- Support for fix/cofix added in Ltac "match" and "lazymatch".
+
+- Ltac backtraces now include trace information about tactics
+  called by OCaml-defined tactics.
+
+- Option "Ltac Debug" now applies also to terms built using Ltac functions.
+
 Tools
 
 - Coq_makefile lets one override or extend the following variables from
@@ -22,20 +38,6 @@ Vernacular Commands
   By default, they are disabled and produce an error. The deprecation
   warning which used to occur when using nested proofs has been removed.
 
-Tactics
-
-- Introduction tactics "intro"/"intros" on a goal which is an
-  existential variable now force a refinement of the goal into a
-  dependent product rather than failing.
-
-Tactic language
-
-- Support for fix/cofix added in Ltac "match" and "lazymatch".
-
-- Ltac backtraces now include trace information about tactics
-  called by OCaml-defined tactics.
-- Option "Ltac Debug" now applies also to terms built using Ltac functions.
-
 Coq binaries and process model
 
 - Before 8.9, Coq distributed a single `coqtop` binary and a set of
@@ -67,9 +69,9 @@ Tools
 
 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.
+- The undocumented "nameless" forms `fix N`, `cofix` have been
+  deprecated; please use `fix ident N /cofix ident` to explicitely
+  name the (co)fixpoint hypothesis to be introduced.
 
 Documentation