Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Adding support for recursive notations of the form "x , .. , y , z". | Hugo Herbelin | 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 |
| |/ / / / / |/| | | | | | |||
* | | | | | | 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 |
| * | | | | | | 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 |
| |/ / / / / |/| | | | | | |||
* | | | | | | 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 |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #896: Prepare De Bruijn universe abstractions, Spin-off: Checker | 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 PR #877: Travis+4.05.0 | Maxime Dénès | 2017-07-20 |
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / / / / |/| | | | | | | | | | | | |||
* | | | | | | | | | | | | Merge branch 'v8.7' | Maxime Dénès | 2017-07-20 |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #745: Add timing scripts | Maxime Dénès | 2017-07-19 |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #855: Deprecate options that were introduced for compatibility with ... | Maxime Dénès | 2017-07-19 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* | \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #770: [proof] Move bullets to their own module. | Maxime Dénès | 2017-07-19 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | * | | | | | | [proofs] Remove circular dependency from Proofview to Goal. | Emilio Jesus Gallego Arias | 2017-07-19 |
| |_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | |||
| | | | | | | | | * | | | | | | [general] Move files to directories matching linking order. | Emilio Jesus Gallego Arias | 2017-07-19 |
| |_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | |||
* | | | | | | | | | | | | | | Merge PR #788: [API] Remove `open API` in ml files in favor of `-open API` flag. | Maxime Dénès | 2017-07-19 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | * | | | | | | [pp] Fix bugs 5651 [incorrect thunk in pretty printer] | Emilio Jesus Gallego Arias | 2017-07-19 |
| |_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | |||
| | | | | | | | | | | | | * | Fix debug trace of typeclasses eauto. | Théo Zimmermann | 2017-07-19 |
| | | | | | | | * | | | | | | Fixing the checker w.r.t. wrongly used abstract universe contexts. | Pierre-Marie Pédrot | 2017-07-19 |
| | | | | | | | | |_|_|_|/ | | | | | | | | |/| | | | |