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.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/doc/RecTutorial/RecTutorial.v b/doc/RecTutorial/RecTutorial.v
index 4b0ab31254..4a17e08182 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
-- 
cgit v1.2.3