index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
adding a test-suite file 4709.v (thanks to the new command Extraction TestCom...
Pierre Letouzey
2017-07-26
*
Extraction: reduce primitive projections in types (fix bug 4709)
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
|
\
*
\
Merge PR #910: Add [opam update] and online repository to gitlab CI script.
Maxime Dénès
2017-07-26
|
\
\
*
\
\
Merge PR #886: Fixing what was presumably a typo in the naming conventions file
Maxime Dénès
2017-07-26
|
\
\
\
*
\
\
\
Merge PR #902: Only perform profile initialization and printing when the flag...
Maxime Dénès
2017-07-26
|
\
\
\
\
*
\
\
\
\
Merge PR #894: Fixing a little location bug with recursive binders
Maxime Dénès
2017-07-26
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #882: Adding a V8.7 compatibility version number.
Maxime Dénès
2017-07-26
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #885: Removing a dummy parameter in some FMapPositive statements.
Maxime Dénès
2017-07-26
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #868: Fix debug trace of typeclasses eauto.
Maxime Dénès
2017-07-26
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #845: Add Z.mod_div lemma to standard library.
Maxime Dénès
2017-07-26
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #905: [api] Remove type equalities from API.
Maxime Dénès
2017-07-26
|
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
Merge PR #857: Extraction: various fixes related with bug 4720
Maxime Dénès
2017-07-26
|
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
Merge PR #859: Extraction TestCompile
Maxime Dénès
2017-07-26
|
\
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
\
Merge PR #808: [api] Put some order in API.mli
Maxime Dénès
2017-07-26
|
\
\
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
\
\
Merge PR #750: Remove deprecated options of ./configure in 8.8
Maxime Dénès
2017-07-26
|
\
\
\
\
\
\
\
\
\
\
\
\
\
\
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
make sure that API-leaks cannot be reintroduced by mistake
Matej Košík
2017-07-26
*
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Makefile.ide: restore a coqide-binaries rule (fix bug 5667)
Pierre Letouzey
2017-07-25
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
[api] Remove type equalities from API.
Emilio Jesus Gallego Arias
2017-07-25
|
|
|
|
_
|
/
/
/
/
/
/
/
/
/
/
|
|
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
|
|
[api] Put modules in order in API.{mli,ml}
Emilio Jesus Gallego Arias
2017-07-25
|
|
/
/
/
/
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 484...
Pierre Letouzey
2017-07-25
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
Adding a V8.7 compatibility version number.
Hugo Herbelin
2017-07-21
|
|
_
|
_
|
_
|
_
|
_
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
|
Merge PR #897: Fix test suite on windows (wrt fake_ide and coq-makefile)
Maxime Dénès
2017-07-21
|
\
\
\
\
\
\
\
\
\
\
\
|
*
|
|
|
|
|
|
|
|
|
|
PMP sold us a Timeout on Windows with 1s resolution. Trying to improve it.
Maxime Dénès
2017-07-21
|
|
|
|
|
|
|
|
|
|
|
*
Add [opam update] and online repository to gitlab CI script.
Gaëtan Gilbert
2017-07-21
|
*
|
|
|
|
|
|
|
|
|
|
Install time command under Cygwin (required for timing scripts).
Maxime Dénès
2017-07-21
|
|
|
|
*
|
|
|
|
|
|
|
Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)
Pierre Letouzey
2017-07-20
|
|
|
|
|
|
_
|
_
|
_
|
_
|
_
|
/
|
|
|
|
|
/
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
|
Merge PR #892: Improve do_split option of typeclass resolution
Maxime Dénès
2017-07-20
|
\
\
\
\
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
fake_ide: do as coqide to find out coqtop path
Enrico Tassi
2017-07-20
|
|
*
|
|
|
|
|
|
|
|
coq_makefile: use System.exists_dir for better portability
Enrico Tassi
2017-07-20
|
|
*
|
|
|
|
|
|
|
|
Windows: Sys.is_dir "foo/" always says no (so we strip trailing slash)
Enrico Tassi
2017-07-20
|
|
*
|
|
|
|
|
|
|
|
coq-makefile: strip windows drive letter when DESTDIR is not empty
Enrico Tassi
2017-07-20
|
|
*
|
|
|
|
|
|
|
|
coq-makefile: treat coq_makefile as any other coq binary
Enrico Tassi
2017-07-20
|
|
*
|
|
|
|
|
|
|
|
more verbose logs for coq-makefile
Enrico Tassi
2017-07-20
|
|
*
|
|
|
|
|
|
|
|
coq-makefile: quote using ' to preserve \ (windows paths)
Enrico Tassi
2017-07-20
|
|
*
|
|
|
|
|
|
|
|
coq-makefile: make test suite detect more errors
Enrico Tassi
2017-07-20
|
|
*
|
|
|
|
|
|
|
|
In fake_ide, call coqtop.exe instead of coqtop on Win32.
Maxime Dénès
2017-07-20
|
|
*
|
|
|
|
|
|
|
|
Avoid using unsupported signals under Windows in fake_ide.
Maxime Dénès
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
|
|
*
|
|
|
|
|
|
|
|
Add AppVeyor infrastructure, launching the test suite under Windows.
Maxime Dénès
2017-07-20
|
|
/
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
Also a less intrusive Profile.init_profile.
Hugo Herbelin
2017-07-20
|
|
|
|
|
|
|
|
*
|
A less intrusive Profile.close_profile.
Hugo Herbelin
2017-07-20
*
|
|
|
|
|
|
|
|
|
Merge PR #900: [proofs] Remove circular dependency from Proofview to Goal.
Maxime Dénès
2017-07-20
|
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
Merge PR #899: [general] Move files to directories so they match linking order.
Maxime Dénès
2017-07-20
|
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
Merge PR #903: Documenting the purity / marshallability invariant of persiste...
Maxime Dénès
2017-07-20
|
\
\
\
\
\
\
\
\
\
\
\
\
|
*
|
|
|
|
|
|
|
|
|
|
|
Documenting the purity / marshallability invariant of persistent states.
Pierre-Marie Pédrot
2017-07-20
*
|
|
|
|
|
|
|
|
|
|
|
|
Merge PR #898: [pp] Fix bugs 5651 [incorrect thunk in pretty printer]
Maxime Dénès
2017-07-20
|
\
\
\
\
\
\
\
\
\
\
\
\
\
[next]