index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
Commit message (
Expand
)
Author
Age
...
*
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
*
Uminus.v : prepare this test file for the use of Fail
letouzey
2013-09-19
*
universes-buraliforti-redef.v : repair a match after Pierre B. syntax changes
letouzey
2013-09-19
*
Fixing some tests from the test-suite.
ppedrot
2013-09-03
*
* test-suite/success/Unicode_utf8:
regisgia
2013-09-02
*
Trickyer test for Paral-ITP
gareuselesinge
2013-08-30
*
Universe counters on slaves are in sync with master
gareuselesinge
2013-08-20
*
Test for Paral-ITP
gareuselesinge
2013-08-08
*
Coqide ported to STM
gareuselesinge
2013-08-08
*
Fix testsuite so that it works with STM
gareuselesinge
2013-08-08
*
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
*
better error message for unexpected renaming (closes #2987)
gareuselesinge
2013-07-29
*
Fixing bug #3093 by adding the asked test case.
ppedrot
2013-07-25
*
More dynamic argument scopes
letouzey
2013-07-17
*
Continuing r16621 on injection intro-patterns:
herbelin
2013-07-10
*
Revising r16550 about providing intro patterns for applying injection:
herbelin
2013-07-09
*
Bugfix: Fixing #3050
ppedrot
2013-06-27
*
Fix [setoid_rewrite] forgetting some evars that are produced when typecheckin...
msozeau
2013-06-10
*
Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as an
herbelin
2013-06-02
*
Fixing a regression in unification introduced in r16205 (error raised
herbelin
2013-05-14
*
Updating some output tests in test-suite:
herbelin
2013-05-09
*
A uniformization step around understand_* and interp_* functions.
herbelin
2013-05-09
*
Protection against "Bad recursive type" in w_unify0 (bug #3036).
herbelin
2013-05-08
*
Declaration of multiple hypotheses or parameters now share typing
herbelin
2013-05-08
*
Share more information between constructors and arity of an inductive
herbelin
2013-05-08
*
Moved isolated test params_ind.v to Inductive.v.
herbelin
2013-05-08
*
Hack to solve a "Bad recursive type" anomaly.
herbelin
2013-05-05
*
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
*
Renaming SearchAbout into Search and Search into SearchHead.
herbelin
2013-04-17
*
Using Parameter instead of Variable in test-suite/output
herbelin
2013-04-17
*
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
*
Continuation of r16346 on filtering local definitions. Refined
herbelin
2013-03-30
*
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
*
Cosmetic code contraction in evarsolve.ml + test sur unification avec let-in.
herbelin
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
*
Using hnf instead of "intro H" for forcing reduction to a product.
herbelin
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
[prev]
[next]