diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-com.tex | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 56cf8b06a7..8d128e6b47 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -193,6 +193,10 @@ Add physical path {\em directory} to the {\ocaml} loadpath. some standard axioms of classical mathematics such as the functional axiom of choice or the principle of description +\item[{\tt -type-in-type}]\ + + This collapses the universe hierarchy of {\Coq} making the logic inconsistent. + \item[{\tt -compat} {\em version}] \mbox{} Attempt to maintain some of the incompatible changes in their {\em version} |