c439a6bc2c
from bugfixes): - Coq compilation made possible with forthcoming ocaml 4.03. - command for locating exists notation in refman changed. - Various improvements of the Reference Manual (especially its html version) - implicit arguments of local definitions fixed (possible source of incompatibilities). - New command "Print Debug GC". - Function cannot define graph. - Optimizing compilation of pattern matching. - Better inference of impossible cases in pattern-matching. - Evar leak in pattern-matching compilation - ill-typed replacement in "change ... with ...". - unbound evars in "change ... with ...". - wrong return clause of a match pattern in Ltac. - cleared local hints for autounfold. - cleared local hints for autounfold. - lost evars in "change ... with ...". - supporting let-ins in constructors for vm_compute - unfortunate typo in compare_height. - unfortunate typos in absorption lemmas over bool. - Full support of utf8 Greek letters (block U0370) in coqdoc
6 lines
308 B
Text
6 lines
308 B
Text
$NetBSD: distinfo,v 1.21 2015/04/25 13:41:18 jaapb Exp $
|
|
|
|
SHA1 (coq-8.4pl6.tar.gz) = c89525295659a805661ef91da24ecfb94e226953
|
|
RMD160 (coq-8.4pl6.tar.gz) = f57f6e5732d3977f3346dda2749f4b9628604018
|
|
Size (coq-8.4pl6.tar.gz) = 4099815 bytes
|
|
SHA1 (patch-Makefile.build) = 3fa72d701a80f363ef637e3cbd0e4c2d410da6c4
|