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
/
closed
Commit message (
Expand
)
Author
Age
*
Fix bug#2080: error message on Ltac name clash with primitive tactics
xclerc
2014-01-10
*
Added test-suite for bug #2990.
Pierre-Marie Pédrot
2013-12-16
*
Better unification for [projT1] and [proj1_sig].
Jason Gross
2013-12-12
*
Fix the refine related test-suite files to account for the new refine.
Arnaud Spiwack
2013-12-06
*
Test case for bug#2848.
xclerc
2013-12-02
*
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-09-20
*
Added test for bug #2846.
ppedrot
2013-08-04
*
Added a test for bug #3062.
ppedrot
2013-08-04
*
Added a test for bug #3088.
ppedrot
2013-08-01
*
Tentative fix for #3054: we refresh universes in a term generated
ppedrot
2013-07-29
*
Fixing bug #3093 by adding the asked test case.
ppedrot
2013-07-25
*
Bugfix: Fixing #3050
ppedrot
2013-06-27
*
Protection against "Bad recursive type" in w_unify0 (bug #3036).
herbelin
2013-05-08
*
Added a unit test for bug #2230.
ppedrot
2013-04-27
*
Finer fix for bug 3017, mark unresolvability only of goals that are
msozeau
2013-04-18
*
Like in r16346, do not filter local definitions (here in the
herbelin
2013-04-17
*
Added regression test for bug #3023 which was solved by Matthieu's
herbelin
2013-04-16
*
Equality: avoid some unprotected List.nth (fix #2837)
letouzey
2013-04-10
*
Enrich test-suite with a test for #3022.
ppedrot
2013-04-08
*
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-25
*
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-21
*
Check a list length before doing a List.chop (fix #3000)
letouzey
2013-03-20
*
Fix for bug #3004 (thanks Hugo!)
letouzey
2013-03-18
*
A slightly more efficient test of well-typedness of restriction of
herbelin
2013-02-21
*
Fixed bug #2981 (anomaly NotASort in Retyping due to collision between
herbelin
2013-02-05
*
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-29
*
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-28
*
Unset Asymmetric Patterns
pboutill
2013-01-18
*
Fixed bug #2930: folded let-in's were hiding a violation to the occur
herbelin
2012-11-25
*
Fixing #2836 (materialize_evar might refine as a side effect the
herbelin
2012-07-29
*
Continuing r15459: it helps testing occur-check early in some
herbelin
2012-07-06
*
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2012-07-05
*
Fixing bug #2817 (occur check was not done up to instantiation of
herbelin
2012-06-20
*
Implicit arguments of Definition are taken from the type when given by the user.
pboutill
2012-04-27
*
Bug 2733 : { } implicits and Fixpoints
pboutill
2012-04-17
*
Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).
herbelin
2012-04-15
*
Repair two tests
letouzey
2012-04-12
*
Generalized the use of evar candidates in type inference unification:
herbelin
2012-03-20
*
Fix bugs related to Program integration.
msozeau
2012-03-19
*
Fixing bug #2732 (anomaly when using the tolerance for writing
herbelin
2012-03-18
[next]