diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-21 21:11:45 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-29 15:36:19 +0200 |
| commit | 435cd91ddb71a59fef3611210b19e9d01fc730f9 (patch) | |
| tree | d7743802868ecf948fc4f8d5e893c72d2f3a87c7 /doc | |
| parent | f78bc2ca33c7bb7eb139e51c2cb74a3a63a040c9 (diff) | |
Documenting option -type-in-type.
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 56cf8b06a..8d128e6b4 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} |