diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-09 01:33:31 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-13 12:13:48 +0200 |
commit | 2243c25c79ab19876ad74452c9cecc7dcc88c67c (patch) | |
tree | f32573eb7d7c4dbdb4493e186bed87c80e61a747 /doc | |
parent | b68e0b4f9ba37d1c2fa5921e1d934b4b38bfdfe7 (diff) |
[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.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/RecTutorial/RecTutorial.tex | 6 | ||||
-rw-r--r-- | doc/RecTutorial/RecTutorial.v | 2 |
2 files changed, 4 insertions, 4 deletions
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 |