From 2243c25c79ab19876ad74452c9cecc7dcc88c67c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
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.
---
 doc/RecTutorial/RecTutorial.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/RecTutorial/RecTutorial.tex')

diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex
index d0884be0dd..01369b9003 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!)
-- 
cgit v1.2.3