aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* #3828 is solved.Gravatar Hugo Herbelin2014-12-16
* Moving #2447 (congruence) to fixed.Gravatar Hugo Herbelin2014-12-16
* Test for #3654.Gravatar Hugo Herbelin2014-12-16
* fix bug #2447 in congruenceGravatar Pierre Corbineau2014-12-16
* Adapted test file for About.Gravatar Pierre Courtieu2014-12-15
* Tests for #3848 and #3854.Gravatar Hugo Herbelin2014-12-15
* About now accepts hypothesis names and goal selector.Gravatar Pierre Courtieu2014-12-15
* Tests for Searchxxx commands added and modified.Gravatar Pierre Courtieu2014-12-15
* Two fixes in unification (bugs #3782 and #3709)Gravatar Matthieu Sozeau2014-12-12
* Test suite: keep message in sync with actual file deletions.Gravatar Xavier Clerc2014-12-11
* New reproduction cases for the test suite.Gravatar Xavier Clerc2014-12-11
* Fixing orientation of postponed subtyping problems.Gravatar Hugo Herbelin2014-12-10
* typoGravatar Enrico Tassi2014-12-10
* test-suite: few tests for ".v -> .vi -> .vo" compilation chainGravatar Enrico Tassi2014-12-10
* Improving evar restriction (this is a risky change, as I remember aGravatar Hugo Herbelin2014-12-07
* Commits on evar-evar unification fixed HoTT_coq_106 and improved theGravatar Hugo Herbelin2014-12-05
* Take benefit of improved name preservation of evars in e2fa65fcc.Gravatar Hugo Herbelin2014-12-04
* Updading test-suite.Gravatar Hugo Herbelin2014-12-03
* When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' ifGravatar Hugo Herbelin2014-12-02
* Fixing test-suite.Gravatar Pierre-Marie Pédrot2014-12-01
* Adding test for bug #3417.Gravatar Pierre-Marie Pédrot2014-11-30
* Test for bug #3485.Gravatar Pierre-Marie Pédrot2014-11-30
* Test for bug #3487.Gravatar Pierre-Marie Pédrot2014-11-30
* Test of bug #3682.Gravatar Pierre-Marie Pédrot2014-11-30
* Fix test flags for fake_ideGravatar Enrico Tassi2014-11-27
* Bug #3804 is actually closed (thanks to Jason Gross for the notification).Gravatar Xavier Clerc2014-11-25
* Tweak some test cases.Gravatar Xavier Clerc2014-11-25
* Adapting to current semantics of "simpl non-evaluable-cst"Gravatar Hugo Herbelin2014-11-25
* Experimenting using unification when matching evar/meta free subtermsGravatar Hugo Herbelin2014-11-25
* Adding test for bug #3248.Gravatar Pierre-Marie Pédrot2014-11-24
* Pass around information on the use of template polymorphism forGravatar Matthieu Sozeau2014-11-23
* Test for closed #2713 and #2876.Gravatar Hugo Herbelin2014-11-22
* Add test-suite file for dependent rewriting example by Vadim Zaliva andGravatar Matthieu Sozeau2014-11-22
* Adding test for bug #3326.Gravatar Pierre-Marie Pédrot2014-11-21
* Adding test for bug #3424.Gravatar Pierre-Marie Pédrot2014-11-21
* Cleaning up closed bugs in test-suite.Gravatar Pierre-Marie Pédrot2014-11-21
* Test for bug #3788.Gravatar Pierre-Marie Pédrot2014-11-21
* Add test-suite file for bug #3804.Gravatar Matthieu Sozeau2014-11-21
* Adding test for bug #3684.Gravatar Pierre-Marie Pédrot2014-11-20
* Fixing a little bug with nested but convertible occurrences in "destruct at".Gravatar Hugo Herbelin2014-11-18
* Fixing detection of occurrences in the presence of nested subterms forGravatar Hugo Herbelin2014-11-18
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Fixing side bug in db37c9f3f32ae7 delaying interpretation of theGravatar Hugo Herbelin2014-11-16
* Use return code to classify anomalies as active open bugs.Gravatar Xavier Clerc2014-11-14
* Add missing "Fail" to test case for bug #2814.Gravatar Xavier Clerc2014-11-14
* Reproduction cases for the test suite.Gravatar Xavier Clerc2014-11-14
* Preserving the good effect of 014e5ac92a on not leaving dangling localGravatar Hugo Herbelin2014-11-14
* Removing yet another source of remaining local definitions.Gravatar Hugo Herbelin2014-11-13
* Adapting output tests to current naming of evars, even if unclearGravatar Hugo Herbelin2014-11-11
* Adding test for bug 3792.Gravatar Pierre-Marie Pédrot2014-11-09