coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-07-24	Add simple test cases for vm and native on primitive projections.	Gaëtan Gilbert

2018-06-15	Add test-suite case for performance, had to use Timeout	Matthieu Sozeau

2018-03-04	[compat] Remove NOOP and alias deprecated options.	Emilio Jesus Gallego Arias
	Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP.
2017-07-27	test-suite: more use of the new command Extraction TestCompile	Pierre Letouzey

2017-06-14	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey
	The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
2016-07-06	Fixed bug #4622.	Matthieu Sozeau

2016-07-06	Disallow dependent case on prim records w/o eta	Matthieu Sozeau

2016-03-10	Primitive projections: protect kernel from erroneous definitions.	Matthieu Sozeau
	E.g., Inductive foo := mkFoo { bla : foo } allowed to define recursive records with eta for which conversion is incomplete. - Eta-conversion only applies to BiFinite inductives - Finiteness information is now checked by the kernel (the constructor types must be strictly non recursive for BiFinite declarations).
2015-11-18	Fixing logical bugs in the presence of let-ins in computiong primitive	Hugo Herbelin
	projections. - lift accounting for the record missing in computing the subst from fields to projections of the record - substitution for parameters should not lift the local definitions - typo in building the latter (subst -> letsubst)
2015-07-22	Extraction: fix primitive projection extraction.	Matthieu Sozeau
	Use expand projection to come back to the projection-as-constant encoding, dealing with parameters correctly.
2014-09-17	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau
	contortions in internalization/externalization. It uses a fully typed version of detyping, requiring the environment, to move from primitive projection applications to regular applications of the eta-expanded version. The kernel is unchanged, and only constrMatching needs compatibility code now.
2014-09-10	Parsing and printing of primitive projections, fix buggy behavior when	Matthieu Sozeau
	implicits do not allow to parse as an application and cleanup code.
2014-09-09	- Fix printing and parsing of primitive projections, including the Set	Matthieu Sozeau
	Printing All cases (bug #3597). - Fix Ltac matching with primitive projections (bug #3598). - Spotted a problem with printing of constants with maximally implicit arguments due to strange "compatibility" interpretation of Arguments [X] as Arguments {X} but didn't fix it entirely yet (might cause incompatibilities).
2014-09-05	Fix primitive projections declarations for inductive records.	Matthieu Sozeau

2014-08-30	Simplify even further the declaration of primitive projections,	Matthieu Sozeau
	now done entirely using declare_mind, which declares the associated constants for primitive records. This avoids a hack related to elimination schemes and ensures that the forward references to constants in the mutual inductive entry are properly declared just after the inductive. This also clarifies (and simplifies) the code of term_typing for constants which does not have to deal with building or checking projections anymore. Also fix printing of universes showing the de Bruijn encoding in a few places.