diff options
| -rw-r--r-- | CHANGES | 4 | ||||
| -rw-r--r-- | doc/refman/RefMan-com.tex | 4 |
2 files changed, 8 insertions, 0 deletions
@@ -32,6 +32,10 @@ Logic projection application. - [pattern x at n], [rewrite x at n] and in general abstraction and selection of occurrences may fail due to the disappearance of parameters. +- New universe polymorphism. +- New option -type-in-type to collapse the universe hierarchy (this makes the + logic inconsistent). + Vernacular commands 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} |