d7c9ff8bb9
Many changes, among them: - Many bugs have been fixed (cf coq-bugs web page) - changed parsing precedence of let/in and fun constructions of Ltac: let x := t in e1; e2 is now parsed as let x := t in (e1;e2). - New primitive "external" for communication with tool external to Coq. - Omega now handles arbitrary precision integers. - Haskell extraction: types of functions are now printed, better unsafeCoerce mechanism, both for hugs and ghc. - Scheme extraction improved, see http://www.pps.jussieu.fr/~letouzey/scheme. - New notation "exists! x:A, P" for unique existence. - New library on String and Ascii characters (contributed by L. Thery). - New library FSets+FMaps of finite sets and maps. - New library QArith on rational numbers. - Few improvements in ZArith potentially exceptionally breaking the compatibility (useless hypothesys of Zgt_square_simpl and Zlt_square_simpl removed; fixed names mentioning letter O instead of digit 0; weaken premises in Z_lt_induction). |
||
|---|---|---|
| .. | ||
| patches | ||
| DESCR | ||
| distinfo | ||
| Makefile | ||
| MESSAGE | ||
| PLIST | ||
| PLIST.opt | ||