| Commit message (Expand) | Author | Age |
|---|
| ... | |
| | | | | | | | | | | | | | * | | | | | [summary] Allow typed projections from global state + rework of internals. |  Emilio Jesus Gallego Arias | 2017-12-09 |
| | | | | | | | | | | | | | * | | | | | [lib] Convenience function for `Dyn.Easy` | Emilio Jesus Gallego Arias | 2017-12-09 |
| | | |_|_|_|_|_|_|_|_|_|_|/ / / / /
| |/| | | | | | | | | | | | | | | |
|
| | | | | | | * | | | | | | | | | | | Remove up-to-conversion matching functions. |  Pierre-Marie Pédrot | 2017-12-09 |
| | | | | | | | | | | | | | * | | | | Remove most uses of function extensionality in Program.Combinators |  Jasper Hugunin | 2017-12-09 |
| | | |_|_|_|_|_|_|_|_|_|_|/ / / /
| |/| | | | | | | | | | | | | | |
|
| | | | | | * | | | | | | | | | | | [ci] Download ci-sf archives into the proper CI build dir. | Emilio Jesus Gallego Arias | 2017-12-09 |
| | |_|_|_|/ / / / / / / / / / /
|/| | | | | | | | | | | | | | |
|
| | * | | | | | | | | | | | | | | Revert "CI: poc Circleci configuration" |  Arnaud Spiwack | 2017-12-08 |
| | * | | | | | | | | | | | | | | CI: poc Circleci configuration | Arnaud Spiwack | 2017-12-08 |
| |/ / / / / / / / / / / / / / |
|
| | | | | | | * / / / / / / / | [makefile] Address #6291: install more development files. | Emilio Jesus Gallego Arias | 2017-12-08 |
| | |_|_|_|_|/ / / / / / / /
|/| | | | | | | | | | | | |
|
| | | | * | | | | | | | | | | Fix a copy-paste error in ci-ltac2. |  Théo Zimmermann | 2017-12-08 |
| * | | | | | | | | | | | | | Merge PR #6334: Remove dead code in Reductionops |  Maxime Dénès | 2017-12-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6158: Allows a level in the raw and glob printers | Maxime Dénès | 2017-12-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6224: Add alienclean target to remove compilation products with no ... | Maxime Dénès | 2017-12-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | * | | | | | | | | | | | [ci] CoLoR has moved to github | Emilio Jesus Gallego Arias | 2017-12-07 |
| * | | | | | | | | | | | | | | | | Merge PR #6267: Fix PR merge script. | Maxime Dénès | 2017-12-07 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/
|/| | | | | | | | | | | | | | | |
|
| | | | | | * | | | | | | | | | | | [default.nix] Add ocpIndent and ocp-index. | Maxime Dénès | 2017-12-07 |
| | |_|_|_|/ / / / / / / / / / /
|/| | | | | | | | | | | | | | |
|
| | | | | | | | * | | | | | | | | Getting rid of pf_matches in Hipattern. | Pierre-Marie Pédrot | 2017-12-07 |
| * | | | | | | | | | | | | | | | Merge PR #6290: Rename update to set, Fixes #6196 | Maxime Dénès | 2017-12-07 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #873: New strategy based on open scopes for deciding which notation ... | Maxime Dénès | 2017-12-07 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6142: Single quotes break on Windows | Maxime Dénès | 2017-12-07 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | 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 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | | | |
|
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Jasper Hugunin
Arnaud Spiwack
Théo Zimmermann
Maxime Dénès
Vincent Laporte
Joachim Breitner
Gaëtan Gilbert
Hugo Herbelin
Paul Steckler
Martin Vassor