Path to this page:
Subject: CVS commit: pkgsrc/lang/coq
From: Jaap Boender
Date: 2020-01-24 16:54:49
Message id: 20200124155449.218A8FBF4@cvs.NetBSD.org
Log Message:
Updated lang/coq to version 8.10.2.
Changes include:
- native 63-bit machine integers;
- a new sort of definitionally proof-irrelevant propositons: SProp;
- private universes for opaque polymorphic constants;
- string notations and numeral notations;
- a new simplex-based proof engine for the tactics lia, nia, lra and nra;
- new introduction patterns for SSReflect;
- a tactic to rewrite under binders: under;
- easy input of non-ASCII symbols in CoqIDE, which now uses GTK3.
and many small improvements and bugfixes.
Files: