index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
Age
Commit message (
Expand
)
Author
2014-12-16
#3828 is solved.
Hugo Herbelin
2014-12-16
Moving #2447 (congruence) to fixed.
Hugo Herbelin
2014-12-16
Test for #3654.
Hugo Herbelin
2014-12-16
fix bug #2447 in congruence
Pierre Corbineau
2014-12-15
Adapted test file for About.
Pierre Courtieu
2014-12-15
Tests for #3848 and #3854.
Hugo Herbelin
2014-12-15
About now accepts hypothesis names and goal selector.
Pierre Courtieu
2014-12-15
Tests for Searchxxx commands added and modified.
Pierre Courtieu
2014-12-12
Two fixes in unification (bugs #3782 and #3709)
Matthieu Sozeau
2014-12-11
Test suite: keep message in sync with actual file deletions.
Xavier Clerc
2014-12-11
New reproduction cases for the test suite.
Xavier Clerc
2014-12-10
Fixing orientation of postponed subtyping problems.
Hugo Herbelin
2014-12-10
typo
Enrico Tassi
2014-12-10
test-suite: few tests for ".v -> .vi -> .vo" compilation chain
Enrico Tassi
2014-12-07
Improving evar restriction (this is a risky change, as I remember a
Hugo Herbelin
2014-12-05
Commits on evar-evar unification fixed HoTT_coq_106 and improved the
Hugo Herbelin
2014-12-04
Take benefit of improved name preservation of evars in e2fa65fcc.
Hugo Herbelin
2014-12-03
Updading test-suite.
Hugo Herbelin
2014-12-02
When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if
Hugo Herbelin
2014-12-01
Fixing test-suite.
Pierre-Marie Pédrot
2014-11-30
Adding test for bug #3417.
Pierre-Marie Pédrot
2014-11-30
Test for bug #3485.
Pierre-Marie Pédrot
2014-11-30
Test for bug #3487.
Pierre-Marie Pédrot
2014-11-30
Test of bug #3682.
Pierre-Marie Pédrot
2014-11-27
Fix test flags for fake_ide
Enrico Tassi
2014-11-25
Bug #3804 is actually closed (thanks to Jason Gross for the notification).
Xavier Clerc
2014-11-25
Tweak some test cases.
Xavier Clerc
2014-11-25
Adapting to current semantics of "simpl non-evaluable-cst"
Hugo Herbelin
2014-11-25
Experimenting using unification when matching evar/meta free subterms
Hugo Herbelin
2014-11-24
Adding test for bug #3248.
Pierre-Marie Pédrot
2014-11-23
Pass around information on the use of template polymorphism for
Matthieu Sozeau
2014-11-22
Test for closed #2713 and #2876.
Hugo Herbelin
2014-11-22
Add test-suite file for dependent rewriting example by Vadim Zaliva and
Matthieu Sozeau
2014-11-21
Adding test for bug #3326.
Pierre-Marie Pédrot
2014-11-21
Adding test for bug #3424.
Pierre-Marie Pédrot
2014-11-21
Cleaning up closed bugs in test-suite.
Pierre-Marie Pédrot
2014-11-21
Test for bug #3788.
Pierre-Marie Pédrot
2014-11-21
Add test-suite file for bug #3804.
Matthieu Sozeau
2014-11-20
Adding test for bug #3684.
Pierre-Marie Pédrot
2014-11-18
Fixing a little bug with nested but convertible occurrences in "destruct at".
Hugo Herbelin
2014-11-18
Fixing detection of occurrences in the presence of nested subterms for
Hugo Herbelin
2014-11-16
Enforcing a stronger difference between the two syntaxes "simpl
Hugo Herbelin
2014-11-16
Fixing side bug in db37c9f3f32ae7 delaying interpretation of the
Hugo Herbelin
2014-11-14
Use return code to classify anomalies as active open bugs.
Xavier Clerc
2014-11-14
Add missing "Fail" to test case for bug #2814.
Xavier Clerc
2014-11-14
Reproduction cases for the test suite.
Xavier Clerc
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-11
Adapting output tests to current naming of evars, even if unclear
Hugo Herbelin
2014-11-09
Adding test for bug 3792.
Pierre-Marie Pédrot
[next]