Module Name:	pkgsrc
Committed By:	tonio
Date:		Sun Feb 25 15:03:52 UTC 2007

Modified Files:
	pkgsrc/lang/coq: Makefile PLIST distinfo
	pkgsrc/lang/coq/patches: patch-aa

Log Message:
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).


To generate a diff of this commit:
cvs rdiff -r1.15 -r1.16 pkgsrc/lang/coq/Makefile
cvs rdiff -r1.4 -r1.5 pkgsrc/lang/coq/PLIST
cvs rdiff -r1.5 -r1.6 pkgsrc/lang/coq/distinfo
cvs rdiff -r1.4 -r1.5 pkgsrc/lang/coq/patches/patch-aa

Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.