CVS commit: pkgsrc/lang/coq

["Antoine Reilles" <tonio%netbsd.org@localhost>]

Module Name:    pkgsrc
Committed By:   tonio
Date:           Mon Mar 28 20:39:26 UTC 2011

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

Log Message:
Update lang/coq to 8.3pl1

Changes from V8.3 to V8.3pl1
o Type inference, notations and implicit arguments bug fixes
- #2448 (alpha-renaming problems with notations internally using binders)
- #2454 (pattern-matching sometimes not supporting type casts)
- fixing combined use of non-implicit and explictly-declared implicit arguments
  in inductive arities
- restored support for using some ident with different scopes in notations
o Ltac and tactics bug fixes
- #2414 (rewrite in not looking for eq_ind in the right module)
- #2433 (new "is_evar"/"has_evar" to restore support for matching evars in Ltac)
- #2453 (dependent destruction)
- loop in dependent destruction
- new "constr_eq" tactic for restoring support for term equality test in Ltac
- setoid rewrite under cases and abstraction fixed
o Coqdoc and documentation bugs
- #2418 (wrong URLs in documentation)
- #2441 (coqdoc bug in Mergesort.v)
- #2445 (correct support for "'" character in coqdoc links to notations)
- fixed wrong use of "moduleid" instead of "module" in coqdoc html indexes
- fixing parsing of Multiplication and Division signs (unicode 0xD7 and 0xF7)
o Compilation
- #2432 (support for compilation with camlp5 6.02.0)
- support for compilation with ocaml >= 3.09.3 restored
o Extraction
- #2413 (prevent type-unsafe optimisations of pattern matching)
- Identifiers of a development aimed to be extracted should
  avoid containing "__", since the extraction make various use of
  this sub-string, leading to potential name clashes. This was
  already so in V8.3, but not announced, as mentionned by #2421.
o Miscellaneous bug fixes
- #2412 (anomaly Ploc.Exc when using Ltac Debug)
- #2419 (redundant opp_compare removed)
- #2427 (Module Functor claims Signature does not match)
- #2431 (compliance of CoqIDE use of mutexes with FreeBSD)
- #2434 (anomaly DuringSyntaxChecking with Local/Global prefixes)
- a few improvements in efficiency


To generate a diff of this commit:
cvs rdiff -u -r1.29 -r1.30 pkgsrc/lang/coq/Makefile
cvs rdiff -u -r1.12 -r1.13 pkgsrc/lang/coq/distinfo
cvs rdiff -u -r1.9 -r0 pkgsrc/lang/coq/patches/patch-aa
cvs rdiff -u -r1.4 -r0 pkgsrc/lang/coq/patches/patch-ab

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