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
*
Merge PR #773: [flags] Remove XML output flag.
Maxime Dénès
2017-08-29
|
\
*
|
Fix coqdoc test-suite target on Windows.
Théo Zimmermann
2017-08-21
*
|
Merge PR #942: solving b1859
Maxime Dénès
2017-08-16
|
\
\
*
\
\
Merge PR #954: Print names of all open blocks
Maxime Dénès
2017-08-16
|
\
\
\
*
\
\
\
Merge PR #841: Timorous fix of bug #5598 on global existing class in sections
Maxime Dénès
2017-08-16
|
\
\
\
\
*
\
\
\
\
Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords wr...
Maxime Dénès
2017-08-16
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #864: Some cleanups after cumulativity for inductive types
Maxime Dénès
2017-08-16
|
\
\
\
\
\
\
|
|
|
|
|
*
|
Adding a test for BZ#1859 as suggested by @tchajed.
Théo Zimmermann
2017-08-15
|
|
|
|
*
|
|
Print names of all open blocks
Tej Chajed
2017-08-06
|
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
[flags] Remove XML output flag.
Emilio Jesus Gallego Arias
2017-08-01
|
|
_
|
_
|
_
|
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).
Maxime Dénès
2017-08-01
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #926: test-suite uses Extraction TestCompile
Maxime Dénès
2017-08-01
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)
Maxime Dénès
2017-08-01
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #834: Adding support for recursive notations of the form "x , .. , y...
Maxime Dénès
2017-08-01
|
\
\
\
\
\
\
\
\
|
|
|
|
|
*
|
|
|
Change the option for cumulativity
Amin Timany
2017-07-31
|
|
|
|
|
*
|
|
|
Add Jason's example of fun-ext with cumulativity
Amin Timany
2017-07-31
|
|
|
|
|
*
|
|
|
Add test for NonCumulative inductives
Amin Timany
2017-07-31
|
|
|
|
|
*
|
|
|
Issue error on monomorphic cumulative inductives
Amin Timany
2017-07-31
|
|
|
|
|
|
|
_
|
/
|
|
|
|
|
|
/
|
|
*
|
|
|
|
/
|
|
closing bug 5315
Julien Forest
2017-07-29
|
|
_
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
|
|
Fixing bug #5671 (specialize unclean wrt Metas).
Hugo Herbelin
2017-07-27
|
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
test-suite: more use of the new command Extraction TestCompile
Pierre Letouzey
2017-07-27
*
|
|
|
|
|
Fix TypeclassDebug.out after conflicting PR merges
Matthieu Sozeau
2017-07-26
|
|
|
*
|
|
test-suite/success/extraction.v : add some Extraction TestCompile
Pierre Letouzey
2017-07-26
|
|
|
*
|
|
Enrich test file 4720.v with a compilation test of the extracted code
Pierre Letouzey
2017-07-26
|
|
_
|
/
/
/
|
/
|
|
|
|
|
|
*
|
|
adding a test-suite file 4709.v (thanks to the new command Extraction TestCom...
Pierre Letouzey
2017-07-26
|
|
/
/
/
|
/
|
|
|
*
|
|
|
Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs 4844...
Maxime Dénès
2017-07-26
|
\
\
\
\
|
|
*
|
|
Adding support for recursive notations of the form "x , .. , y , z".
Hugo Herbelin
2017-07-26
|
|
/
/
/
|
/
|
|
|
*
|
|
|
Merge PR #857: Extraction: various fixes related with bug 4720
Maxime Dénès
2017-07-26
|
\
\
\
\
|
|
*
|
|
Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 484...
Pierre Letouzey
2017-07-25
|
|
/
/
/
|
/
|
|
|
|
*
|
|
Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)
Pierre Letouzey
2017-07-20
*
|
|
|
fake_ide: do as coqide to find out coqtop path
Enrico Tassi
2017-07-20
*
|
|
|
more verbose logs for coq-makefile
Enrico Tassi
2017-07-20
*
|
|
|
coq-makefile: make test suite detect more errors
Enrico Tassi
2017-07-20
*
|
|
|
Remove trailing CR before diff in output and misc tests.
Maxime Dénès
2017-07-20
*
|
|
|
Print failure logs on appveyor.
Maxime Dénès
2017-07-20
*
|
|
|
Remove non-terminating Timeout tests from Hints.v.
Maxime Dénès
2017-07-20
*
|
|
|
Make coqlib relative in test suite (revert 024a7ab20b0)
Maxime Dénès
2017-07-20
|
/
/
/
*
|
|
Merge PR #869: Enforce alternating separators in typeclass debug output
Maxime Dénès
2017-07-20
|
\
\
\
*
\
\
\
Merge branch 'v8.7'
Maxime Dénès
2017-07-20
|
\
\
\
\
|
|
|
*
|
Removing testing unsupported Next.
Hugo Herbelin
2017-07-19
|
*
|
|
|
Merge PR #745: Add timing scripts
Maxime Dénès
2017-07-19
|
|
\
\
\
\
|
|
|
|
*
|
Adding a coqdoc target to test-suite.
Hugo Herbelin
2017-07-17
*
|
|
|
|
|
Getting rid of abstraction breaking code in tclABSTRACT.
Pierre-Marie Pédrot
2017-07-14
*
|
|
|
|
|
Removing the uses of abstraction-breaking code in Lemmas.
Pierre-Marie Pédrot
2017-07-13
|
|
_
|
_
|
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel
Maxime Dénès
2017-07-13
|
\
\
\
\
\
|
|
|
|
*
|
format pairs of items for pr_depth to get alternating separators
Paul Steckler
2017-07-12
|
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
*
|
|
Deprecate options that were introduced for compatibility with 8.5.
Théo Zimmermann
2017-07-11
|
|
/
/
/
|
/
|
|
|
|
*
|
|
Fix nonsensical universe abstraction in the kernel.
Pierre-Marie Pédrot
2017-07-11
|
*
|
|
Properly handling polymorphic inductive subtyping in the kernel.
Pierre-Marie Pédrot
2017-07-11
|
*
|
|
Cleaning up the implementation of module subtyping in the kernel.
Pierre-Marie Pédrot
2017-07-11
[next]