diff options
| author | tonio <tonio> | 2011-03-28 20:39:26 +0000 |
|---|---|---|
| committer | tonio <tonio> | 2011-03-28 20:39:26 +0000 |
| commit | 9b242d016f9ef995e5495ec7043d0bcbaa9ac815 (patch) | |
| tree | 5a3d0fe7c8d5c8c57db80f6add51c2cc56f16b04 /lang/coq/distinfo | |
| parent | ef52dfeb8557833f2f55bb56ff8fd49e58ebcefc (diff) | |
| download | pkgsrc-9b242d016f9ef995e5495ec7043d0bcbaa9ac815.tar.gz | |
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
Diffstat (limited to 'lang/coq/distinfo')
| -rw-r--r-- | lang/coq/distinfo | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/lang/coq/distinfo b/lang/coq/distinfo index 85aff64b172..8a6e9a540f7 100644 --- a/lang/coq/distinfo +++ b/lang/coq/distinfo @@ -1,8 +1,6 @@ -$NetBSD: distinfo,v 1.12 2010/11/14 20:53:02 tonio Exp $ +$NetBSD: distinfo,v 1.13 2011/03/28 20:39:26 tonio Exp $ -SHA1 (coq-8.3.tar.gz) = 6c6472b6a41429e78d979eacd8ff58bd6f6c9da4 -RMD160 (coq-8.3.tar.gz) = 9e42266001c0a22b39662be86960a05e454fc2fb -Size (coq-8.3.tar.gz) = 3736420 bytes -SHA1 (patch-aa) = 851efa1859b4d8dc7bad549792a5966b549f868e -SHA1 (patch-ab) = f20f78c936e18ca195933375f37fc5b816827604 +SHA1 (coq-8.3pl1.tar.gz) = 3fae9fa2fd6f39c9fb3c0b67fcd5e71f1e7a5f9f +RMD160 (coq-8.3pl1.tar.gz) = 687983bcaca723299b6ea902a1e1b07338209d55 +Size (coq-8.3pl1.tar.gz) = 3756961 bytes SHA1 (patch-ac) = 59516eb44aa6cedb4f897b5ac3e8fe0aa69aba0f |