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 unit tests to test suite
Paul Steckler
2018-05-16
*
Merge PR #7484: Fix non-portable shebang in test-suite.
Enrico Tassi
2018-05-16
|
\
*
|
[ssr] import ssreflect test suite from math-comp
Enrico Tassi
2018-05-15
*
|
Merge PR #7502: Fixing little printing bug with "Locate" on recursive notations
Emilio Jesus Gallego Arias
2018-05-14
|
\
\
*
\
\
Merge PR #7479: Move 4722 (dangling symlink) to misc tests, remove dangling s...
Gaëtan Gilbert
2018-05-14
|
\
\
\
|
|
*
|
Fixing a bug in printing the body of a located notation.
Hugo Herbelin
2018-05-13
|
|
/
/
|
/
|
|
|
*
|
Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repo
Ralf Jung
2018-05-13
*
|
|
Merge PR #7477: Support for notations with autonomous only-parsing and only-p...
Emilio Jesus Gallego Arias
2018-05-13
|
\
\
\
*
\
\
\
Merge PR #7470: use at least 6 Xs in mktemp filename templates
Gaëtan Gilbert
2018-05-11
|
\
\
\
\
|
|
|
|
*
Fix non-portable shebang in test-suite.
Théo Zimmermann
2018-05-11
|
|
_
|
_
|
/
|
/
|
|
|
*
|
|
|
Merge PR #7363: [ci] Fix another issue with the timing tests
Gaëtan Gilbert
2018-05-11
|
\
\
\
\
|
|
|
*
|
Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).
Hugo Herbelin
2018-05-10
|
|
|
*
|
Fixes part 1 of #7462 (only-printing not to override existing interp rule).
Hugo Herbelin
2018-05-10
|
|
|
|
/
|
|
*
/
use at least 6 Xs in mktemp filename templates
Sven M. Hallberg
2018-05-09
|
|
|
/
*
|
/
test for coqc -o
Enrico Tassi
2018-05-09
|
|
/
|
/
|
*
|
Merge PR #7134: When an error comes from loading the prelude, tell it happene...
Emilio Jesus Gallego Arias
2018-05-03
|
\
\
|
*
|
Making explicit that errors happen in one of five executation phases.
Hugo Herbelin
2018-05-02
*
|
|
Make "intro"/"intros" progress on existential variables.
Hugo Herbelin
2018-05-02
|
/
/
*
|
Strict focusing using Default Goal Selector.
Gaëtan Gilbert
2018-04-29
|
*
[ci] Fix another issue with the timing tests
Jason Gross
2018-04-26
*
|
Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.
Hugo Herbelin
2018-04-26
|
/
*
test suite: clean more things (glob, MExtraction.out, distclean aux)
Gaëtan Gilbert
2018-04-22
*
test suite: print message for failing tests as they come
Gaëtan Gilbert
2018-04-22
*
test suite Makefile: do not use %.stamp for subsystem targets
Gaëtan Gilbert
2018-04-22
*
Merge PR #7237: [ssr] fix delayed clears (fix #7045)
Maxime Dénès
2018-04-16
|
\
*
|
[ltac] Deprecate nameless fix/cofix.
Emilio Jesus Gallego Arias
2018-04-13
|
*
[ssr] fix delayed clears (fix #7045)
Enrico Tassi
2018-04-13
|
/
*
Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by removin...
Jason Gross
2018-04-12
|
\
*
\
Merge PR #500: Move bugs that have been closed on Bugzilla
Maxime Dénès
2018-04-12
|
\
\
*
\
\
Merge PR #7087: Congruence tactic engine update
Pierre-Marie Pédrot
2018-04-12
|
\
\
\
|
|
*
|
Fix the status of some resolved bugs
Tej Chajed
2018-04-11
|
|
/
/
|
/
|
|
*
|
|
Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while look...
Emilio Jesus Gallego Arias
2018-04-09
|
\
\
\
*
\
\
\
Merge PR #7176: Fix #6956: Uncaught exception in bytecode compilation
Pierre-Marie Pédrot
2018-04-09
|
\
\
\
\
*
\
\
\
\
Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)
Maxime Dénès
2018-04-09
|
\
\
\
\
\
|
|
*
|
|
|
Fix #6956: Uncaught exception in bytecode compilation
Maxime Dénès
2018-04-06
*
|
|
|
|
|
Improve shell scripts
zapashcanon
2018-04-05
|
|
|
|
|
*
Fix #5981, bugs/opened/3263.v is non-deterministic by removing the test.
Théo Zimmermann
2018-04-05
|
|
_
|
_
|
_
|
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.
Hugo Herbelin
2018-04-04
|
\
\
\
\
\
|
|
_
|
/
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR #6407: Fix #6404 - Print tactics called by ML tactics
Pierre-Marie Pédrot
2018-04-04
|
\
\
\
\
\
|
|
|
*
|
|
ssr: check cleared hyps do exist (fix #7050)
Enrico Tassi
2018-04-04
|
|
_
|
/
/
/
|
/
|
|
|
|
*
|
|
|
|
Update coq_makefile timing test
Jason Gross
2018-04-02
|
*
|
|
|
Fix #6404 - Print tactics called by ML tactics
Jason Gross
2018-04-02
|
/
/
/
/
*
|
|
|
Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)
Pierre-Marie Pédrot
2018-04-01
|
\
\
\
\
*
|
|
|
|
Change Implicit Arguments to Arguments in test-suite
Jasper Hugunin
2018-03-30
|
|
*
|
|
Fix #6257: anomaly with Printing Projections and Context.
Gaëtan Gilbert
2018-03-30
|
|
|
*
|
Fixes #7110 ("as" untested while looking for notation for nested patterns).
Hugo Herbelin
2018-03-29
*
|
|
|
|
Fix #6631: Derive Plugin gives "Anomaly: more than one statement".
Pierre-Marie Pédrot
2018-03-29
|
|
/
/
/
|
/
|
|
|
|
*
|
|
Supporting fix/cofix in Ltac pattern-matching (wish #7092).
Hugo Herbelin
2018-03-28
|
|
/
/
*
|
|
Merge PR #7090: stm: don't propagate side effects when editing a proof
Emilio Jesus Gallego Arias
2018-03-28
|
\
\
\
*
\
\
\
Merge PR #6961: [test-suite] Add backtracking test for `Load`.
Enrico Tassi
2018-03-28
|
\
\
\
\
[next]