index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
bugs
/
closed
/
shouldsucceed
Age
Commit message (
Expand
)
Author
2013-09-20
Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.
xclerc
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-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-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-01-18
Unset Asymmetric Patterns
pboutill
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
2012-06-20
Fixing bug #2817 (occur check was not done up to instantiation of
herbelin
2012-04-27
Implicit arguments of Definition are taken from the type when given by the user.
pboutill
2012-04-17
Bug 2733 : { } implicits and Fixpoints
pboutill
2012-04-15
Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).
herbelin
2012-04-12
Repair two tests
letouzey
2012-03-20
Generalized the use of evar candidates in type inference unification:
herbelin
2012-03-19
Fix bugs related to Program integration.
msozeau
2012-03-18
Fixing bug #2732 (anomaly when using the tolerance for writing
herbelin
2012-03-13
Fixing vm_compute bug #2729 (function used to decompose constructors
herbelin
2012-01-05
Backtracking on r14876 (fix for bug #2267): extra scopes might be
herbelin
2012-01-04
Fixing Arguments Scope bug when too many scopes are given (bug #2667).
herbelin
2011-11-21
Extend the computation of dependencies in pattern-matching compilation
herbelin
2011-11-17
Fixing bug #2640 and variants of it (inconsistency between when and
herbelin
2011-11-16
Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).
herbelin
2011-10-25
Regression tests for bugs #2613 and #2616.
herbelin
2011-10-25
New strategy to infer return predicate of match construct when
herbelin
2011-10-24
Mod_subst: Attempt to fix #2608
letouzey
2011-10-18
Fix bug #2473 due to wrong folding of the evar environment
msozeau
2011-10-18
Fix inductive coercion code in Program (bug #2378)
msozeau
2011-10-17
Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing z...
msozeau
2011-10-12
test-suite: non-regression test for bug #2603
letouzey
2011-10-11
Added test for bug #2615
herbelin
2011-10-07
fsetdec : non-atomic elements are now transformed as variables first (fix #2464)
letouzey
2011-10-07
Improved handling of element equalities in fsetdec (fix #2467)
letouzey
2011-09-15
Omega aware of Z.pred (fix #1912)
letouzey
2011-09-15
Re-allowing assumptions during proofs seems safe now (fix #2411)
letouzey
2011-06-18
Relaxed the constraint introduced in r14190 that froze the existing
herbelin
2011-06-18
Partial backtrack on wrong r14204: bug #2490 still open.
herbelin
[next]