Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Browse files

Merged README.markdown

  • Loading branch information...
commit bd6630ca48feda320b3b2d87a47e86c222f6fd5c 2 parents 46b1125 + 7b9a36f
@andrejbauer authored
Showing with 11 additions and 4 deletions.
  1. +11 −4 README.markdown
15 README.markdown
@@ -10,11 +10,18 @@ The HoTT library is a development of homotopy-theoretic ideas in the Coq proof a
It draws many ideas from Vladimir Voevodsky's
[Foundations]( library.
-Installation details are explained in the file `INSTALL.txt`.
+Installation details are explained in the file `INSTALL.txt`. You will need to compile a
+custom version of Coq which supports the `-relevant-equality` and
+`-warn-universe-inconsistency` command-line options. We hope to have these options pushed
+into standard Coq.
+If you are looking for an older version of HoTT which works with standard Coq, have a look
+at the one tagged as `pure-coq-8.3`. Note however that we do not support the old
+library anymore.
It is possible to use the HoTT library directly on the command line with the `hoqtop`
script, but who does that?
@@ -28,7 +35,7 @@ without asking, you should probably customize set the variable `proof-prog-name-
At the moment there is no `hoqide` equivalent of `coqide`, but getting one is high on our
to-do list.
The library is released under the permissive BSD 2-clause license, see the file
`LICENSE.txt` for further information. In brief, this means you can do whatever you like

0 comments on commit bd6630c

Please sign in to comment.
Something went wrong with that request. Please try again.