| Commit message (Expand) | Author | Age |
* | Introduce an option to allow nested lemma, and turn it off by default. | Théo Zimmermann | 2018-05-17 |
* | 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 |