coq - The formal proof system

Age	Commit message (Expand)	Author
2016-02-13	Do not give a name to anonymous evars anymore. See bug #4547.	Pierre-Marie Pédrot
2015-12-05	Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)	Hugo Herbelin
2015-11-07	Tests for syntax "Show id" and [id]:tac (shelved or not).	Hugo Herbelin
2014-12-04	Take benefit of improved name preservation of evars in e2fa65fcc.	Hugo Herbelin
2014-12-02	When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if	Hugo Herbelin
2014-11-18	Fixing a little bug with nested but convertible occurrences in "destruct at".	Hugo Herbelin
2014-11-14	Preserving the good effect of 014e5ac92a on not leaving dangling local	Hugo Herbelin
2014-11-13	Removing yet another source of remaining local definitions.	Hugo Herbelin
2014-11-06	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-03	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-02	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-10-31	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-27	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-26	Fixing destruct/induction with a using clause on a non-inductive type,	Hugo Herbelin
2014-10-25	This commit introduces changes in induction and destruct.	Hugo Herbelin
2014-08-28	Fixing an unnatural selection of subterms larger than expected in the	Hugo Herbelin
2014-08-18	Fixing unification of subterms identified by patterns.	Hugo Herbelin
2011-10-25	Fixing "destruct" test.	herbelin
2011-10-22	Use full conversion for checking type of holes in destruct over a	herbelin
2011-06-10	Fixing another bug with "_" intro pattern.	herbelin
2011-06-10	Made use of "_" in repeated use of intros_patterns work (with	herbelin
2009-10-04	Removal of trailing spaces.	serpyc
2009-09-27	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-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-02-23	Add support for dependent "destruct" over terms in dependent types.	herbelin
2008-06-18	Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk	herbelin
2008-04-13	Bugs, nettoyage, et améliorations diverses	herbelin
2006-12-13	Dépliage du terme d'induction avant suppression quand celui-ci est un	herbelin
2006-05-31	Fusion destruct.v et Destruct.v (MacOS X ne sait pas distinguer la casse	herbelin
2005-12-21	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin
2004-06-02	commentaire	herbelin
2004-05-20	Protection du destruct pour vérifier que ce n'est pas une anomalie, à défa...	herbelin
2004-05-02	Ajout test bug 711	herbelin