CVS log for pkgsrc/lang/coq/distinfo

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).

This form allows you to request diff's between any two revisions of a file. You may select a symbolic revision name using the selection box or you may type in a numeric name using the type-in text box.