| Commit message (Expand) | Author | Age |
... | |
* | | | | | | | | | | | | | | | | | Merge PR #6277: Qualified import in coqchk | Maxime Dénès | 2017-12-07 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | | * | | [configure] fix spelling mistake | Vincent Laporte | 2017-12-07 |
* | | | | | | | | | | | | | | | | | | Merge PR #6322: Fix #6286 (non stability of micromega csdp cache rebuilding) | Maxime Dénès | 2017-12-07 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6321: Use preference for ocamlfind in configure | Maxime Dénès | 2017-12-07 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6316: Correct typo | Maxime Dénès | 2017-12-07 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6309: [default.nix] needs ncurses for the test-suite | Maxime Dénès | 2017-12-07 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6303: Remove redundant Zcase from the checker. | Maxime Dénès | 2017-12-07 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | | * | Additional rewrite lemmas on Ensembles, in Powerset_facts | Joachim Breitner | 2017-12-06 |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/
|/| | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | * | | | | | | Getting rid of pf_is_matching in Funind. | Pierre-Marie Pédrot | 2017-12-06 |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / /
|/| | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | * | | | | | | | Getting rid of the Update constructor in Reductionops. | Pierre-Marie Pédrot | 2017-12-06 |
| | | | | | | | | | | | | * | | | | | | | Getting rid of the Shift constructor in Reductionops. | Pierre-Marie Pédrot | 2017-12-06 |
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / /
|/| | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | * | | | | | Overlay for Equations. | Gaëtan Gilbert | 2017-12-06 |
| | | | | | | | | | | | | | | | | * | | Linter: skip PRs older than the linter. | Gaëtan Gilbert | 2017-12-06 |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ /
|/| | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | * | | | | Fix #6323: stronger restrict universe context vs abstract. | Gaëtan Gilbert | 2017-12-06 |
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / /
|/| | | | | | | | | | | | | | | | |
|
| | | | | * | | | | | | | | | | | | Replacing Hashtbl.add by Hashtbl.replace in micromega cache building. | Hugo Herbelin | 2017-12-05 |
| | | | | | | | | * | | | | | | | | Rename update to set, fixes #6196 | Paul Steckler | 2017-12-05 |
| | | | * | | | | | | | | | | | | | use preference for ocamlfind | Paul Steckler | 2017-12-05 |
| |_|_|/ / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | * | | Don't Add LoadPath on CoqIDE startup, #6153 | Paul Steckler | 2017-12-05 |
| | | | | |_|_|_|_|_|_|_|_|/ /
| | | | |/| | | | | | | | | | |
|
| | | * / | | | | | | | | | | | Correct typo | Martin Vassor | 2017-12-05 |
| |_|/ / / / / / / / / / / /
|/| | | | | | | | | | | | | |
|
| | * | | | | | | | | | | | | [default.nix] explain ncurses dependency | Vincent Laporte | 2017-12-05 |
* | | | | | | | | | | | | | | Merge PR #890: Global universe declarations | Maxime Dénès | 2017-12-05 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6266: Safe unmarshalling in the checker | Maxime Dénès | 2017-12-05 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | * | [configure] adds a `select_command` function | Vincent Laporte | 2017-12-05 |
* | | | | | | | | | | | | | | | | Merge PR #6301: [vernac] Couple of tweaks missing from previous PRs. | Maxime Dénès | 2017-12-05 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6306: Adding a test for #6304 (a bug with "fix" in notations). | Maxime Dénès | 2017-12-05 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6300: Clarify operation of sequences, fixes #6095 | Maxime Dénès | 2017-12-05 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212 | Maxime Dénès | 2017-12-05 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6293: Check for Num lib if OCaml >= 4.06, fixes #6162 | Maxime Dénès | 2017-12-05 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6302: Uninstall doc dir, not dev (which is not installed), fixes #6007 | Maxime Dénès | 2017-12-05 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6287: Add merlin to default.nix | Maxime Dénès | 2017-12-05 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6210: More complete not-fully-applied error messages, #6145 | Maxime Dénès | 2017-12-05 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | | | * | [configure] fix detection of `md5sum` | Vincent Laporte | 2017-12-04 |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/
|/| | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | * | | | | | | | | | | [default.nix] needs ncurses for the test-suite | Vincent Laporte | 2017-12-04 |
| |_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | * | | | | | | | | | | | | | [vernac] Couple of tweaks missing from previous PRs. | Emilio Jesus Gallego Arias | 2017-12-04 |
| |_|_|_|_|_|_|/ / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | |
|
| | | | | | | * | | | | | | | | | | | | | Adding a test for #6304 (bug with fix in notations). | Hugo Herbelin | 2017-12-03 |
| |_|_|_|_|_|/ / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | * | | | | | | | | | | Remove redundant Zcase from the checker. | Pierre-Marie Pédrot | 2017-12-02 |
| |_|_|_|_|_|_|_|/ / / / / / / / / /
|/| | | | | | | | | | | | | | | | | |
|
| | | * | | | | | | | | | | | | | | | uninstall doc dir, not dev (which is not installed), #6007 | Paul Steckler | 2017-12-01 |
| |_|/ / / / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | |
|
| | | * | | | | | | | | | | | | | | check for Num lib if OCaml >= 4.06, #6162 | Paul Steckler | 2017-12-01 |
| | | | |_|_|_|_|_|_|/ / / / / /
| | | |/| | | | | | | | | | | | |
|
| | | | | * | | | | | | | | | | | clarify operation of sequences, #6095 | Paul Steckler | 2017-12-01 |
| | | | |/ / / / / / / / / / /
| | | |/| | | | | | | | | | | |
|
| | | | | | * | | | | | | | | | Update CHANGES | Matthieu Sozeau | 2017-12-01 |
| | | | | | * | | | | | | | | | Cleanup API for registering universe binders. | Matthieu Sozeau | 2017-12-01 |
| | | | | | * | | | | | | | | | [refman] Expand a little on global universes. | Matthieu Sozeau | 2017-12-01 |
| | | | | | * | | | | | | | | | Tests for global universe declarations | Matthieu Sozeau | 2017-12-01 |
| | | | | | * | | | | | | | | | Proper nametab handling of global universe names | Matthieu Sozeau | 2017-12-01 |
| |_|_|_|_|/ / / / / / / / /
|/| | | | | | | | | | | | | |
|
| | | | | | * | | | | | | | | Documenting the -Q flag of coqchk. | Pierre-Marie Pédrot | 2017-12-01 |
* | | | | | | | | | | | | | | Merge PR #736: [ci] Test coqchk on the CompCert target. | Maxime Dénès | 2017-12-01 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6256: CI: better ocaml warning checks | Maxime Dénès | 2017-12-01 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6276: Coqchk accepts filenames | Maxime Dénès | 2017-12-01 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6233: [proof] [api] Rename proof types in preparation for functiona... | Maxime Dénès | 2017-12-01 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|/ / / / / / / / / / /
|/| | | | | | | | | | | | | | | | |
|
* | | | | | | | | | | | | | | | | | Merge PR #1049: Remove obsolete locality | Maxime Dénès | 2017-11-30 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|