index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
bugs
Commit message (
Expand
)
Author
Age
*
Univs: fix bug #4031: wrong folding of sigma in change.
Matthieu Sozeau
2015-02-12
*
Adding test for bug #3786.
Pierre-Marie Pédrot
2015-02-11
*
Adding test for bug #3900.
Pierre-Marie Pédrot
2015-02-11
*
Fixing #4001 (missing type constraints when building return clause of match).
Hugo Herbelin
2015-02-10
*
Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ...
Hugo Herbelin
2015-02-10
*
Fixing #4018 (uncaught exception on non-equality in intros [=]).
Hugo Herbelin
2015-02-10
*
Test for bug #4012.
Pierre-Marie Pédrot
2015-02-10
*
Test for bug #3798.
Pierre-Marie Pédrot
2015-01-25
*
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-17
*
Revert "Adapting two files from test-suite to now forbidden Require's in modu...
Maxime Dénès
2015-01-17
*
Revert "Update test for #3363 now that Require is forbidden inside modules."
Maxime Dénès
2015-01-17
*
Revert "Fix files in test-suite having to do with Require inside modules."
Maxime Dénès
2015-01-17
*
Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"
Matthieu Sozeau
2015-01-16
*
TCs: Properly handle Hint Extern with conclusions of the form _ -> _
Matthieu Sozeau
2015-01-13
*
Fix test-suite file, we were testing that no anomaly was raised
Matthieu Sozeau
2015-01-13
*
Fix files in test-suite having to do with Require inside modules.
Maxime Dénès
2015-01-12
*
Update test for #3363 now that Require is forbidden inside modules.
Maxime Dénès
2015-01-12
*
Fixing test for bug #2830.
Pierre-Marie Pédrot
2015-01-06
*
kernel/ind Change interface of declare_mind and declare_mutual
Matthieu Sozeau
2015-01-05
*
Adapting two files from test-suite to now forbidden Require's in modules.
Hugo Herbelin
2015-01-04
*
Fixing #3896 (incorrect sigma given to printer).
Hugo Herbelin
2015-01-03
*
Fixing #3895 (thanks to PMP for diagnosis).
Hugo Herbelin
2015-01-03
*
Fixing #3892: Ensure that notation variables do not capture names
Hugo Herbelin
2014-12-30
*
Fixing wrong notation level in #3295.
Hugo Herbelin
2014-12-19
*
#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
*
Tests for #3848 and #3854.
Hugo Herbelin
2014-12-15
*
Two fixes in unification (bugs #3782 and #3709)
Matthieu Sozeau
2014-12-12
*
New reproduction cases for the test suite.
Xavier Clerc
2014-12-11
*
Commits on evar-evar unification fixed HoTT_coq_106 and improved the
Hugo Herbelin
2014-12-05
*
Updading test-suite.
Hugo Herbelin
2014-12-03
*
When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if
Hugo Herbelin
2014-12-02
*
Fixing test-suite.
Pierre-Marie Pédrot
2014-12-01
*
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-30
*
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
*
Adding test for bug #3248.
Pierre-Marie Pédrot
2014-11-24
*
Pass around information on the use of template polymorphism for
Matthieu Sozeau
2014-11-23
*
Test for closed #2713 and #2876.
Hugo Herbelin
2014-11-22
*
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-21
*
Adding test for bug #3684.
Pierre-Marie Pédrot
2014-11-20
*
Add missing "Fail" to test case for bug #2814.
Xavier Clerc
2014-11-14
[next]