c439a6bc2c
from bugfixes): - Coq compilation made possible with forthcoming ocaml 4.03. - command for locating exists notation in refman changed. - Various improvements of the Reference Manual (especially its html version) - implicit arguments of local definitions fixed (possible source of incompatibilities). - New command "Print Debug GC". - Function cannot define graph. - Optimizing compilation of pattern matching. - Better inference of impossible cases in pattern-matching. - Evar leak in pattern-matching compilation - ill-typed replacement in "change ... with ...". - unbound evars in "change ... with ...". - wrong return clause of a match pattern in Ltac. - cleared local hints for autounfold. - cleared local hints for autounfold. - lost evars in "change ... with ...". - supporting let-ins in constructors for vm_compute - unfortunate typo in compare_height. - unfortunate typos in absorption lemmas over bool. - Full support of utf8 Greek letters (block U0370) in coqdoc |
||
|---|---|---|
| .. | ||
| patches | ||
| DESCR | ||
| distinfo | ||
| Makefile | ||
| MESSAGE | ||
| options.mk | ||
| PLIST | ||