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
*
Fixing #7700 (section variables bound to abbreviations were not found).
Hugo Herbelin
2018-06-10
*
add test for #7595
Ralf Jung
2018-06-07
*
Merge PR #7077: Preserving canonical structure of return predicate in vm_comp...
Maxime Dénès
2018-06-05
|
\
*
\
Merge PR #7663: test suite: make target to regenerate failing output tests
Enrico Tassi
2018-06-05
|
\
\
*
|
|
Fix #7631: native_compute fails to compile an example in Coq 8.8
Maxime Dénès
2018-06-04
*
|
|
Merge PR #7315: An attempt to clarify error message for Arguments needing "re...
Maxime Dénès
2018-06-04
|
\
\
\
|
|
|
*
Tests for part of #7068 and for #7076 (vm/native_compute and return predicate).
Hugo Herbelin
2018-06-04
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR #7229: Deprecate implicit tactic solving.
Hugo Herbelin
2018-06-04
|
\
\
\
|
|
|
*
test suite: make target to regenerate failing output tests
Gaëtan Gilbert
2018-06-04
*
|
|
|
Merge PR #7199: Fixes #7195: missing freshness condition in Ltac pattern-matc...
Matthieu Sozeau
2018-06-04
|
\
\
\
\
*
\
\
\
\
Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.
Matthieu Sozeau
2018-06-04
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomaly
Matthieu Sozeau
2018-06-04
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #7189: Fix #5539: algebraic universe produced by cases.
Matthieu Sozeau
2018-06-04
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ta...
Matthieu Sozeau
2018-06-04
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #7552: Fix #7539: Checker does not properly handle negative coinduct...
Matthieu Sozeau
2018-06-04
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found".
Matthieu Sozeau
2018-06-04
|
\
\
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
|
*
|
|
Deprecate implicit tactic solving.
Pierre-Marie Pédrot
2018-06-04
|
|
_
|
_
|
_
|
_
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.
Maxime Dénès
2018-06-04
|
\
\
\
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
Merge PR #7578: Allow make clean to work on a fresh clone
Enrico Tassi
2018-05-31
|
\
\
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
*
|
|
|
Fix #7113: Program Let Fixpoint in section causes anomaly
Gaëtan Gilbert
2018-05-30
*
|
|
|
|
|
|
|
|
|
|
Fix #6951: Unexpected error during scheme creation.
Pierre-Marie Pédrot
2018-05-29
|
|
_
|
_
|
_
|
_
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
Add test for #7333: vm_compute segfaults / Anomaly with cofix
Maxime Dénès
2018-05-29
|
*
|
|
|
|
|
|
|
|
Allow make clean to work on a fresh clone
Jason Gross
2018-05-25
|
|
|
|
|
|
|
|
|
*
An attempt to clarify error message for Arguments needing "rename" flag.
Hugo Herbelin
2018-05-25
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
Fix #7323: coqchk puts polymorphic univs of inductive in global env
Gaëtan Gilbert
2018-05-24
*
|
|
|
|
|
|
|
|
Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constants
Pierre-Marie Pédrot
2018-05-24
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant inst...
Pierre-Marie Pédrot
2018-05-24
|
\
\
\
\
\
\
\
\
\
\
|
|
|
|
|
*
|
|
|
|
|
Fix #7586: Anomaly "Uncaught exception Not_found".
Pierre-Marie Pédrot
2018-05-23
|
|
_
|
_
|
_
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
Merge PR #7567: Clean-up dead file in test-suite.
Enrico Tassi
2018-05-23
|
\
\
\
\
\
\
\
\
\
\
|
|
_
|
_
|
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
Add test cases from #7554
Tej Chajed
2018-05-20
|
|
|
|
|
*
|
|
|
|
Fix #7539: Checker does not properly handle negative coinductive types.
Pierre-Marie Pédrot
2018-05-18
|
|
_
|
_
|
_
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
Clean-up dead file in test-suite.
Théo Zimmermann
2018-05-18
|
/
/
/
/
/
/
/
/
*
|
|
|
|
|
|
|
Merge PR #7451: Introduce an option to allow nested lemma, and turn it off by...
Emilio Jesus Gallego Arias
2018-05-17
|
\
\
\
\
\
\
\
\
|
*
|
|
|
|
|
|
|
Introduce an option to allow nested lemma, and turn it off by default.
Théo Zimmermann
2018-05-17
*
|
|
|
|
|
|
|
|
Modify make system to include Makefile.common in the test suite
Gaëtan Gilbert
2018-05-16
*
|
|
|
|
|
|
|
|
unit tests: add .merlin
Gaëtan Gilbert
2018-05-16
*
|
|
|
|
|
|
|
|
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
|
\
\
\
\
\
\
\
\
\
\
|
|
|
|
|
|
*
|
|
|
|
Fix #4403: insufficient handling of type-in-type in kernel.
Gaëtan Gilbert
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
|
|
|
|
/
/
/
/
/
/
/
[next]
Hugo Herbelin
Ralf Jung
Maxime Dénès
Enrico Tassi
Gaëtan Gilbert
Matthieu Sozeau
Pierre-Marie Pédrot
Jason Gross
Tej Chajed
Théo Zimmermann
Emilio Jesus Gallego Arias
Paul Steckler