| Age | Commit message (Expand) | Author |
|---|
| 2019-01-24 | Make `Instance` without a body always open a proof. | Maxime Dénès |
| 2018-05-17 | Introduce an option to allow nested lemma, and turn it off by default. | Théo Zimmermann |
| 2017-11-08 | Merge PR #922: New beta-iota compatibility refinements | Maxime Dénès |
| 2017-10-19 | Moving bug numbers to BZ# format in the test-suite. | Théo Zimmermann |
| 2017-08-21 | Fixing a new regresssion with 8.4 wrt to βι-normalization of created hyps. | Hugo Herbelin |
| 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 |
