e691571c08
Main changes: Includes a new tactic (nsatz, standing for Hilbert's NullStellensatz, that extends ring to systems of polynomial equations) and a few new libraries (a certification of mergesort, a new library of finite sets with computational and logical contents separated). This version also comes with many improvements of existing features, especially regarding the tactics, the module system, extraction, the type classes, the program command, libraries, coqdoc. Here is an excerpt: * new operator <+ for conveniently chaining application of functors * new round of extension of the modular library of arithmetic * support for matching terms with binders in Ltac, * linking notations in coqdoc, * quote tactic now working on arbitrary expressions, * Lemma and co accept parameters that are automatically introduced, * interactive proofs in module types, * a beautifying coqc option for pretty-printing files See the file CHANGES for a full log of changes.
8 lines
405 B
Text
8 lines
405 B
Text
$NetBSD: distinfo,v 1.12 2010/11/14 20:53:02 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 (patch-ac) = 59516eb44aa6cedb4f897b5ac3e8fe0aa69aba0f
|