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
*
Add regression tests for 3188 and 3265
Jason Gross
2014-04-22
*
Adding a test for bug #2923.
Pierre-Marie Pédrot
2014-04-20
*
Adding a test for bug #3285.
Pierre-Marie Pédrot
2014-04-20
*
better description of bug 3251
Enrico Tassi
2014-04-10
*
coqtop -batch refuses Back 1 but accepts Undo.
Pierre Boutillier
2014-04-10
*
By resolution of the CoqWG, instantiate must not be used now that refine works
Pierre Boutillier
2014-04-10
*
No more Coersion in Init.
Pierre Boutillier
2014-04-10
*
Define [projT3] and [proj3_sig]
Jason Gross
2014-04-10
*
Test case for bug 3037
Jason Gross
2014-04-10
*
Test case for 3164
Jason Gross
2014-04-10
*
Test case for bug 3262
Jason Gross
2014-04-10
*
Test case for bug #3217
Jason Gross
2014-04-10
*
Add a regression test for bug 3001
Jason Gross
2014-04-10
*
Add another critical bug to the test-suite.
Maxime Dénès
2014-04-09
*
Adapt test-suite to -I is ML only
Pierre Boutillier
2014-04-09
*
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-05
*
Remove option -g as it is non-portable yet does not have any effect on the te...
Guillaume Melquiond
2014-04-04
*
Add a test case for bug 3251
Jason Gross
2014-04-02
*
Fixing bug #2900 (evar/evar unif was supposed to be treated in
Hugo Herbelin
2014-04-01
*
test for apply + TC resolution
Enrico Tassi
2014-03-26
*
nanoPG: better copy/paste
Enrico Tassi
2014-03-13
*
Never suppress the typing constraint of bound variables whose name was
Pierre-Marie Pédrot
2014-03-01
*
Pos.compare_cont takes the comparison as first argument
Pierre Boutillier
2014-02-28
*
test-suite: opaque term -> opaque proof
Pierre Boutillier
2014-02-28
*
test-suite: New names for vars but the expected invariant is preserved
Pierre Boutillier
2014-02-28
*
Fix output test-suite 'simpl tactic' -> 'reduction tactics'
Pierre Boutillier
2014-02-28
*
fake_ide: ported to spawn
Enrico Tassi
2014-02-10
*
Adding a test for bug #3023.
Pierre-Marie Pédrot
2014-01-25
*
Test case containing a proof of false due to a DeBruijn off-by-one error in the
Maxime Dénès
2014-01-15
*
rename Paral-ITP demo file
Enrico Tassi
2014-01-13
*
Paral-ITP demo: better comments
Enrico Tassi
2014-01-13
*
STM: fix very simple demo
Enrico Tassi
2014-01-13
*
Fix bug#2080: error message on Ltac name clash with primitive tactics
xclerc
2014-01-10
*
fix simple test for paral-itp
Enrico Tassi
2014-01-06
*
Add a test suite file for Ltac's "+" tactical.
Arnaud Spiwack
2014-01-06
*
Test case for the buggy commutative cut subterm rule.
Maxime Dénès
2013-12-21
*
micromega: removal of spurious Export; addition of Lia.v encapsulating lia an...
Frédéric Besson
2013-12-20
*
test-suite/output/Notations : evar number change
Pierre Boutillier
2013-12-19
*
Missing Fail in r16792
Pierre Boutillier
2013-12-19
*
test guard condition against feature incompatible with prop-ext
Bruno Barras
2013-12-17
*
Tentative fix of the guardedness checker by Christine and me. All stdlib and ...
Matthieu Sozeau
2013-12-17
*
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
*
Remove duplicate test-suite file.
Arnaud Spiwack
2013-12-06
*
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
*
Test suite: update output reference.
xclerc
2013-12-02
*
Print logical name rather than path (thus allowing reproducible tests).
xclerc
2013-12-02
*
Testsuite: flatten the 'bugs/opened' directory.
xclerc
2013-11-29
[next]