diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/common/macros.tex | 4 | ||||
| -rw-r--r-- | doc/refman/Classes.tex | 9 | ||||
| -rw-r--r-- | doc/refman/RefMan-com.tex | 5 | ||||
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 7 |
4 files changed, 20 insertions, 5 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 0a4251a373..81def1674c 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -94,8 +94,8 @@ \newcommand{\gallina}{\textsc{Gallina}} \newcommand{\Gallina}{\textsc{Gallina}} \newcommand{\CoqIDE}{\textsc{CoqIDE}} -\newcommand{\ocaml}{\textsc{Objective Caml}} -\newcommand{\camlpppp}{\textsc{Camlp4}} +\newcommand{\ocaml}{\textsc{OCaml}} +\newcommand{\camlpppp}{\textsc{Camlp5}} \newcommand{\emacs}{\textsc{GNU Emacs}} \newcommand{\ProofGeneral}{\textsc{Proof General}} \newcommand{\CIC}{\textsc{Cic}} diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 22c75b4fc8..cab6739998 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -462,11 +462,18 @@ abbreviate a type, like {\tt relation A := A -> A -> Prop}. This is equivalent to {\tt Hint Transparent,Opaque} {\ident} {\tt: typeclass\_instances}. +\subsection{\tt Set Typeclasses Axioms Are Instances} +\optindex{Typeclasses Axioms Are Instances} + +This option (off by default since 8.8) automatically declares axioms +whose type is a typeclass at declaration time as instances of that +class. + \subsection{\tt Set Typeclasses Dependency Order} \optindex{Typeclasses Dependency Order} This option (on by default since 8.6) respects the dependency order between -subgoals, meaning that subgoals which are depended on by other subgoals +subgoals, meaning that subgoals which are depended on by other subgoals come first, while the non-dependent subgoals were put before the dependent ones previously (Coq v8.5 and below). This can result in quite different performance behaviors of proof search. diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 8b1fc7c8f3..b4d9f60ebc 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -299,8 +299,9 @@ The following command-line options are recognized by the commands {\tt \section{Compiled libraries checker ({\tt coqchk})} -The {\tt coqchk} command takes a list of library paths as argument. -The corresponding compiled libraries (.vo files) are searched in the +The {\tt coqchk} command takes a list of library paths as argument, described +either by their logical name or by their physical filename, which must end in +{\tt .vo}. The corresponding compiled libraries (.vo files) are searched in the path, recursively processing the libraries they depend on. The content of all these libraries is then type-checked. The effect of {\tt coqchk} is only to return with normal exit code in case of success, diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 60cd8b73a4..3ebeba178a 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -10,6 +10,8 @@ defined object referred by {\qualid}. \begin{ErrMsgs} \item {\qualid} \errindex{not a defined object} +\item \errindex{Universe instance should have length} $n$. +\item \errindex{This object does not support universe names.} \end{ErrMsgs} \begin{Variants} @@ -27,6 +29,11 @@ constructor, abbreviation, \ldots), long name, type, implicit arguments and argument scopes. It does not print the body of definitions or proofs. +\item {\tt Print {\qualid}@\{names\}.}\\ +This locally renames the polymorphic universes of {\qualid}. +An underscore means the raw universe is printed. +This form can be used with {\tt Print Term} and {\tt About}. + %\item {\tt Print Proof {\qualid}.}\comindex{Print Proof}\\ %In case \qualid\ denotes an opaque theorem defined in a section, %it is stored on a special unprintable form and displayed as |