index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
bugs
Age
Commit message (
Expand
)
Author
2014-04-10
Add a regression test for bug 3001
Jason Gross
2014-04-05
Test for bug #3142, actually duplicate of #3262.
Hugo Herbelin
2014-04-05
Fixing bug #3228 (fixing precedence of ltac variables over variables in env).
Hugo Herbelin
2014-04-02
Add a test case for bug 3251
Jason Gross
2014-04-01
Fixing bug #2900 (evar/evar unif was supposed to be treated in
Hugo Herbelin
2014-01-25
Adding a test for bug #3023.
Pierre-Marie Pédrot
2014-01-10
Fix bug#2080: error message on Ltac name clash with primitive tactics
xclerc
2013-12-19
Missing Fail in r16792
Pierre Boutillier
2013-12-16
Added test-suite for bug #2990.
Pierre-Marie Pédrot
2013-12-12
Better unification for [projT1] and [proj1_sig].
Jason Gross
2013-12-06
Fix the refine related test-suite files to account for the new refine.
Arnaud Spiwack
2013-12-02
Test case for bug#2848.
xclerc
2013-11-29
Testsuite: flatten the 'bugs/opened' directory.
xclerc
2013-09-20
Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.
xclerc
2013-09-20
Get rid of "shouldfail" subdirectory by moving tests to parent directory.
xclerc
2013-09-20
Wrong bug identifier.
xclerc
2013-09-20
Update test for bug 2846 in order to use "Fail".
xclerc
2013-09-20
Use "Fail" rather than rely on exit code.
xclerc
2013-08-04
Added test for bug #2846.
ppedrot
2013-08-04
Added a test for bug #3062.
ppedrot
2013-08-01
Added a test for bug #3088.
ppedrot
2013-07-29
Tentative fix for #3054: we refresh universes in a term generated
ppedrot
2013-07-25
Fixing bug #3093 by adding the asked test case.
ppedrot
2013-06-27
Bugfix: Fixing #3050
ppedrot
2013-05-08
Protection against "Bad recursive type" in w_unify0 (bug #3036).
herbelin
2013-04-27
Added a unit test for bug #2230.
ppedrot
2013-04-18
Finer fix for bug 3017, mark unresolvability only of goals that are
msozeau
2013-04-17
Like in r16346, do not filter local definitions (here in the
herbelin
2013-04-16
Added regression test for bug #3023 which was solved by Matthieu's
herbelin
2013-04-10
Equality: avoid some unprotected List.nth (fix #2837)
letouzey
2013-04-08
Enrich test-suite with a test for #3022.
ppedrot
2013-03-25
Enrich test-suite with a test for #2928
letouzey
2013-03-25
Enrich test-suite with a test for #2734
letouzey
2013-03-25
Add the test-case of bug 2750 in the test-suite
letouzey
2013-03-21
Robust display of NotConvertibleTypeField errors (fix #3008, #2995)
letouzey
2013-03-21
Firstorder: record with defined field aren't conjonctions (fix #2629)
letouzey
2013-03-21
Printmod: fresh fake namespaces for non-visible modules (fix #2668, #2983)
letouzey
2013-03-20
Check a list length before doing a List.chop (fix #3000)
letouzey
2013-03-18
Fix for bug #3004 (thanks Hugo!)
letouzey
2013-02-21
A slightly more efficient test of well-typedness of restriction of
herbelin
2013-02-05
Fixed bug #2981 (anomaly NotASort in Retyping due to collision between
herbelin
2013-01-29
Added a file for testing regression of bug #2955 (anomaly in simpl in
herbelin
2013-01-29
Fixing bug #2969 (admit failing after Grab Existential Variables due
herbelin
2013-01-28
Fixed bug #2966 (de Bruijn error in computation of heads for coercions).
herbelin
2013-01-28
Fixing one part of #2830 (anomaly "defined twice" due to nested calls to
herbelin
2013-01-18
Unset Asymmetric Patterns
pboutill
2012-11-25
Fixed bug #2930: folded let-in's were hiding a violation to the occur
herbelin
2012-07-29
Fixing #2836 (materialize_evar might refine as a side effect the
herbelin
2012-07-06
Continuing r15459: it helps testing occur-check early in some
herbelin
2012-07-05
ZArith + other : favor the use of modern names instead of compat notations
letouzey
[prev]
[next]