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 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
|
|
*
|
|
|
Add timing scripts
Jason Gross
2017-07-11
|
|
/
/
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR #863: Fixing environment in warning "Projection value has no head co...
Maxime Dénès
2017-07-07
|
\
\
\
\
\
|
|
/
/
/
/
|
/
|
|
|
|
|
*
|
|
|
Fixing environment in warning "Projection value has no head constant".
Hugo Herbelin
2017-07-07
*
|
|
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-07-04
|
\
\
\
\
\
*
|
|
|
|
|
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
|
|
/
/
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR#843: closing bug #5618 introduce by PR 828
Maxime Dénès
2017-06-30
|
\
\
\
\
\
|
*
|
|
|
|
closing bug #5618 introduce by PR 828
Julien Forest
2017-06-29
|
|
|
*
|
|
A fix for #5598 (no discharge of Existing Classes referring to local variables).
Hugo Herbelin
2017-06-28
*
|
|
|
|
|
Merge PR#810: An attempt to fix a failure of test deps-checksum.sh fails with...
Maxime Dénès
2017-06-27
|
\
\
\
\
\
\
|
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR#826: Put plugin exports in the right compatibility file
Maxime Dénès
2017-06-26
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR#828: closing bug #4250
Maxime Dénès
2017-06-26
|
\
\
\
\
\
\
\
|
|
|
_
|
/
/
/
/
|
|
/
|
|
|
|
|
|
|
|
|
|
*
|
Reorganizing functions to find the relative position of an hypothesis.
Hugo Herbelin
2017-06-25
|
|
|
|
|
*
|
Moving "assert" (internally "Cut") to the new proof engine.
Hugo Herbelin
2017-06-25
|
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR#794: Cleanup of ltac cmxs
Maxime Dénès
2017-06-23
|
\
\
\
\
\
\
|
|
*
|
|
|
|
closing bug #4250
Julien Forest
2017-06-23
|
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
Add tests for handling of warnings
Tej Chajed
2017-06-23
|
|
*
|
|
|
Add test-suite file for funind, extraction with compat 8.6
Jason Gross
2017-06-22
|
|
/
/
/
/
|
/
|
|
|
|
|
|
*
|
|
Should fix a false negative reported by deps-order.sh.
Hugo Herbelin
2017-06-21
|
|
/
/
/
|
/
|
|
|
*
|
|
|
Merge PR#807: romega: fix a slowdown
Maxime Dénès
2017-06-20
|
\
\
\
\
[prev]
[next]
Hugo Herbelin
Pierre Letouzey
Matthieu Sozeau
Maxime Dénès
Enrico Tassi
Pierre-Marie Pédrot
Paul Steckler
Théo Zimmermann
Jason Gross
Julien Forest
Tej Chajed