coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Add test-suite case for performance, had to use Timeout	Matthieu Sozeau	2018-06-15
\|
*	[compat] Remove NOOP and alias deprecated options.	Emilio Jesus Gallego Arias	2018-03-04
\| \| \| \| \| \| \|	Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP.
*	test-suite: more use of the new command Extraction TestCompile	Pierre Letouzey	2017-07-27
\|
*	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
*	Fixed bug #4622.	Matthieu Sozeau	2016-07-06
\|
*	Disallow dependent case on prim records w/o eta	Matthieu Sozeau	2016-07-06
\|
*	Primitive projections: protect kernel from erroneous definitions.	Matthieu Sozeau	2016-03-10
\| \| \| \| \| \| \| \| \|	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).
*	Fixing logical bugs in the presence of let-ins in computiong primitive	Hugo Herbelin	2015-11-18
\| \| \| \| \| \| \| \| \|	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)
*	Extraction: fix primitive projection extraction.	Matthieu Sozeau	2015-07-22
\| \| \| \|	Use expand projection to come back to the projection-as-constant encoding, dealing with parameters correctly.
*	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau	2014-09-17
\| \| \| \| \| \| \| \|	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.
*	Parsing and printing of primitive projections, fix buggy behavior when	Matthieu Sozeau	2014-09-10
\| \| \| \|	implicits do not allow to parse as an application and cleanup code.
*	- Fix printing and parsing of primitive projections, including the Set	Matthieu Sozeau	2014-09-09
\| \| \| \| \| \| \| \|	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).
*	Fix primitive projections declarations for inductive records.	Matthieu Sozeau	2014-09-05
\|
*	Simplify even further the declaration of primitive projections,	Matthieu Sozeau	2014-08-30
	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.