Up to [cvs.NetBSD.org] / pkgsrc / lang / coq
Request diff between arbitrary revisions
Default branch: MAIN
Current tag: pkgsrc-2007Q1-base
Revision 1.6 / (download) - annotate - [select for diffs], Sun Feb 25 15:03:52 2007 UTC (17 years, 1 month ago) by tonio
Branch: MAIN
CVS Tags: pkgsrc-2007Q3-base,
pkgsrc-2007Q3,
pkgsrc-2007Q2-base,
pkgsrc-2007Q2,
pkgsrc-2007Q1-base,
pkgsrc-2007Q1
Changes since 1.5: +5 -5
lines
Diff to previous 1.5 (colored)
Update lang/coq to 8.1 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).