pkgsrc/lang/coq/distinfo

$NetBSD: distinfo,v 1.30 2018/04/09 11:29:23 jaapb Exp $

SHA1 (coq-8.7.2.tar.gz) = 0175cc658aa2c93167572a33e9e39fc63f591258
RMD160 (coq-8.7.2.tar.gz) = 2fd5c59e0143061e4253d68e8839ae3822d7a614
SHA512 (coq-8.7.2.tar.gz) = 6117ef243c62805996a21952016acaaf21db6d1b539fc813c19c897e100f45cde2bee7c9fb045b269a241b79306c656969ca8051e3212ea2090f6d7c1afad5a8
Size (coq-8.7.2.tar.gz) = 5754360 bytes
SHA1 (patch-Makefile.common) = d84cb2a94227e163855f35abebe71f4ec51839fc
Updated lang/coq to version 8.7.2. This fixes a critical bug in the VM handling of universes, and adds various other minor fixes and improvements. 2018-04-09 13:29:23 +02:00			$NetBSD: distinfo,v 1.30 2018/04/09 11:29:23 jaapb Exp $
By popular demand, move coq-7.4 from math to lang in order to be consistent with prior art (e.g. lang/twelf). Coq is a Proof Assistant for a Logical Framework known as the Calculus of Inductive Constructions. It allows the interactive construction of formal proofs, and also the manipulation of functional programs consistently with their specifications. 2003-03-22 21:21:16 +01:00
Updated lang/coq to version 8.7.2. This fixes a critical bug in the VM handling of universes, and adds various other minor fixes and improvements. 2018-04-09 13:29:23 +02:00			`SHA1 (coq-8.7.2.tar.gz) = 0175cc658aa2c93167572a33e9e39fc63f591258`
			`RMD160 (coq-8.7.2.tar.gz) = 2fd5c59e0143061e4253d68e8839ae3822d7a614`
			`SHA512 (coq-8.7.2.tar.gz) = 6117ef243c62805996a21952016acaaf21db6d1b539fc813c19c897e100f45cde2bee7c9fb045b269a241b79306c656969ca8051e3212ea2090f6d7c1afad5a8`
			`Size (coq-8.7.2.tar.gz) = 5754360 bytes`
Updated lang/coq to version 8.7.0. Includes many improvements and bugfixes (none that seem to be breaking backwards compatibility though), see the CHANGELOG. For packaging: - camlp4 support removed, package now uses camlp5 exclusively - fix for PR pkg/52651 2017-11-03 12:20:28 +01:00			`SHA1 (patch-Makefile.common) = d84cb2a94227e163855f35abebe71f4ec51839fc`