index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
coqchk
Commit message (
Expand
)
Author
Age
*
Merge PR #7552: Fix #7539: Checker does not properly handle negative coinduct...
Matthieu Sozeau
2018-06-04
|
\
*
|
Fix #7323: coqchk puts polymorphic univs of inductive in global env
Gaëtan Gilbert
2018-05-24
|
*
Fix #7539: Checker does not properly handle negative coinductive types.
Pierre-Marie Pédrot
2018-05-18
*
|
Fix #7327: coqchk subtyping of polymorphic constants
Gaëtan Gilbert
2018-04-23
*
|
Fix #6798: coqchk ignores ugraph when comparing constant instances
Gaëtan Gilbert
2018-04-20
|
/
*
Delayed weak constraints for cumulative inductive types.
Gaëtan Gilbert
2018-03-09
*
Allow using cumulativity without forcing strict constraints.
Gaëtan Gilbert
2018-03-09
*
Add test case for #5747
Maxime Dénès
2018-01-25
*
Adding a test for coqchk bug #6619.
Pierre-Marie Pédrot
2018-01-20
*
Ensuring all .v files end with a newline to make "sed -i" work better on them.
Hugo Herbelin
2017-08-21
*
Change the option for cumulativity
Amin Timany
2017-07-31
*
Clean up universes of constants and inductives
Amin Timany
2017-06-16
*
Move (part of) tests from checker to success
Amin Timany
2017-06-16
*
Checker add test for non-trivial constraints
Amin Timany
2017-06-16
*
Change the option to Set Inductive Cumulativity
Amin Timany
2017-06-16
*
Correct coqchk reduction
Amin Timany
2017-06-16
*
Add test-suite checks for coqchk with constraints
Jason Gross
2017-05-30
*
Checker: Fix bug #4282
Matthieu Sozeau
2015-07-07
*
new test for coqchk
Enrico Tassi
2014-12-26