coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #922: New beta-iota compatibility refinements	Maxime Dénès	2017-11-08
\|\
* \|	Moving bug numbers to BZ# format in the test-suite.	Théo Zimmermann	2017-10-19
\| *	Fixing a new regresssion with 8.4 wrt to βι-normalization of created hyps.	Hugo Herbelin	2017-08-21
\|/
*	Do not give a name to anonymous evars anymore. See bug #4547.	Pierre-Marie Pédrot	2016-02-13
*	Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)	Hugo Herbelin	2015-12-05
*	Tests for syntax "Show id" and [id]:tac (shelved or not).	Hugo Herbelin	2015-11-07
*	Take benefit of improved name preservation of evars in e2fa65fcc.	Hugo Herbelin	2014-12-04
*	When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if	Hugo Herbelin	2014-12-02
*	Fixing a little bug with nested but convertible occurrences in "destruct at".	Hugo Herbelin	2014-11-18
*	Preserving the good effect of 014e5ac92a on not leaving dangling local	Hugo Herbelin	2014-11-14
*	Removing yet another source of remaining local definitions.	Hugo Herbelin	2014-11-13
*	Restoring clear_flag (thanks a lot to jonikelee to notice it).	Hugo Herbelin	2014-11-06
*	Optimizing when to clear generalized hypotheses in destruct.	Hugo Herbelin	2014-11-06
*	Removing "destruct" test not yet working.	Hugo Herbelin	2014-11-06
*	Subtle swap of lines to preserve VarInstance src field before checking	Hugo Herbelin	2014-11-03
*	Fix to 844431761 on improving elimination with indices, getting rid of	Hugo Herbelin	2014-11-03
*	Improving elimination with indices, getting rid of intrusive residual	Hugo Herbelin	2014-11-02
*	Some reorganization of the code for destruct/induction:	Hugo Herbelin	2014-11-02
*	Fixing file destruct.v.	Hugo Herbelin	2014-11-02
*	Enlarge the cases where the like first selection is used in destruct.	Hugo Herbelin	2014-10-31
*	Listing a few examples of destruct showing unsatisfactory behaviors.	Hugo Herbelin	2014-10-31
*	Avoid "destruct H" to apply on H itself when H is a section variable.	Hugo Herbelin	2014-10-31
*	Making destruct on idents with maximal implicit arguments working, by	Hugo Herbelin	2014-10-27
*	Ensuring compatibility when an hypothesis used for destruct is	Hugo Herbelin	2014-10-27
*	Fixing clash in test destruct.v.	Hugo Herbelin	2014-10-27
*	Fixing destruct/induction with a using clause on a non-inductive type,	Hugo Herbelin	2014-10-26
*	This commit introduces changes in induction and destruct.	Hugo Herbelin	2014-10-25
*	Fixing an unnatural selection of subterms larger than expected in the	Hugo Herbelin	2014-08-28
*	Fixing unification of subterms identified by patterns.	Hugo Herbelin	2014-08-18
*	Fixing "destruct" test.	herbelin	2011-10-25
*	Use full conversion for checking type of holes in destruct over a	herbelin	2011-10-22
*	Fixing another bug with "_" intro pattern.	herbelin	2011-06-10
*	Made use of "_" in repeated use of intros_patterns work (with	herbelin	2011-06-10
*	Removal of trailing spaces.	serpyc	2009-10-04
*	Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.	herbelin	2009-09-27
*	Delay the choice of eliminator in destruct/induction until we know if	herbelin	2009-09-27
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Add support for dependent "destruct" over terms in dependent types.	herbelin	2009-02-23
*	Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk	herbelin	2008-06-18
*	Bugs, nettoyage, et améliorations diverses	herbelin	2008-04-13
*	Dépliage du terme d'induction avant suppression quand celui-ci est un	herbelin	2006-12-13
*	Fusion destruct.v et Destruct.v (MacOS X ne sait pas distinguer la casse	herbelin	2006-05-31
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-21
*	commentaire	herbelin	2004-06-02
*	Protection du destruct pour vérifier que ce n'est pas une anomalie, à défa...	herbelin	2004-05-20
*	Ajout test bug 711	herbelin	2004-05-02