diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/LICENSE | 10 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 10 |
2 files changed, 0 insertions, 20 deletions
diff --git a/doc/LICENSE b/doc/LICENSE index ada22e6690..0aa0d629e8 100644 --- a/doc/LICENSE +++ b/doc/LICENSE @@ -25,16 +25,6 @@ the PostScript, PDF and html outputs) are copyright (c) INRIA distributed under the terms of the Lesser General Public License version 2.1 or later. -The FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo -Herbelin, Florent Kirchner, Benjamin Monate, and Julien Narboux. All -documents (the LaTeX source and the PostScript, PDF and html outputs) -are copyright (c) INRIA 2004-2006. The material connected to the FAQ -(Coq for the Clueless) may be distributed only subject to the terms -and conditions set forth in the Open Publication License, v1.0 or -later (the latest version is presently available at -http://www.opencontent.org/openpub/). Options A and B are *not* -elected. - The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre Castéran and Eduardo Gimenez. All related documents (the LaTeX and BibTeX sources and the PostScript, PDF and html outputs) are copyright diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index c4c0435c5f..0a4d0ef9aa 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1156,16 +1156,6 @@ without having to cut manually the proof in smaller lemmas. It may be useful to generate lemmas minimal w.r.t. the assumptions they depend on. This can be obtained thanks to the option below. -\begin{quote} -\optindex{Shrink Abstract} -{\tt Set Shrink Abstract} -\end{quote} -\emph{Deprecated since 8.7} - -When set (default), all lemmas generated through \texttt{abstract {\tacexpr}} -and \texttt{transparent\_abstract {\tacexpr}} are quantified only over the -variables that appear in the term constructed by \texttt{\tacexpr}. - \begin{Variants} \item \texttt{abstract {\tacexpr} using {\ident}}.\\ Give explicitly the name of the auxiliary lemma. |