5582ef25d8
Changes include: - native 63-bit machine integers; - a new sort of definitionally proof-irrelevant propositons: SProp; - private universes for opaque polymorphic constants; - string notations and numeral notations; - a new simplex-based proof engine for the tactics lia, nia, lra and nra; - new introduction patterns for SSReflect; - a tactic to rewrite under binders: under; - easy input of non-ASCII symbols in CoqIDE, which now uses GTK3. and many small improvements and bugfixes. |
||
|---|---|---|
| .. | ||
| patches | ||
| DESCR | ||
| distinfo | ||
| Makefile | ||
| MESSAGE | ||
| options.mk | ||
| PLIST | ||