Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * | | | | | | Statment -> Statement | Hugo Herbelin | 2018-06-03 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | * | | | | | | | | | | Fixing typos in file Berardi.v | Hugo Herbelin | 2018-06-03 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | |_|_|/ / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | |/| | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7682: Fixes #7641: more detailed message about disjunctive patterns... | Emilio Jesus Gallego Arias | 2018-06-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7689: configure: fix warning printing | Emilio Jesus Gallego Arias | 2018-06-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7637: Fix an outdated comment refering to lib/dnet.mli | Pierre-Marie Pédrot | 2018-06-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | configure: fix warning printing | Gaëtan Gilbert | 2018-06-03 | |
| |/ / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Further sharing in CList. | Hugo Herbelin | 2018-06-03 | |
| | | | | | | | | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Cleaning, documentation, uniformisation of the Coq extension of List. | Hugo Herbelin | 2018-06-03 | |
| |_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7683: [lib] Fix wrong deprecation annotations. | Pierre-Marie Pédrot | 2018-06-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fixes #7641: more detailed message for disjunctive patterns with different vars. | Hugo Herbelin | 2018-06-03 | |
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7656: CI for QuickChick and ext-lib | Emilio Jesus Gallego Arias | 2018-06-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Update .gitlab to use newer ocaml | Leonidas Lampropoulos | 2018-06-02 | |
| | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [lib] Fix wrong deprecation annotations. | Emilio Jesus Gallego Arias | 2018-06-03 | |
| |/ / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7681: Fixes #7636: location missing on deprecated compatibility not... | Emilio Jesus Gallego Arias | 2018-06-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | QuickChick CI | Leonidas Lampropoulos | 2018-06-02 | |
| |/ / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7680: [ci] Expose updated `OCAMLPATH` for CI users. | Gaëtan Gilbert | 2018-06-02 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fixes #7636: location missing on deprecated compatibility notations. | Hugo Herbelin | 2018-06-02 | |
| |/ / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | | | | | | | | * | | | | | | | | | | Refuse to parse empty [Context] command. | Gaëtan Gilbert | 2018-06-02 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [ci] Expose updated `OCAMLPATH` for CI users. | Emilio Jesus Gallego Arias | 2018-06-02 | |
| | | | | | | | | | | | | | | | | | | | | * | | | | | | | | | | | | | | [appveyor] Use OCaml version 4.06.1 in the Windows build. | Emilio Jesus Gallego Arias | 2018-06-02 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7234: Reduce circular dependency constants <-> projections | Maxime Dénès | 2018-06-01 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |/ / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7570: [api] Move `Constrexpr` to the `interp` module. | Maxime Dénès | 2018-06-01 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7537: Improve the Gallina chapter of the reference manual. | Maxime Dénès | 2018-06-01 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7606: Allow more than one signature and name per Sphinx object | Maxime Dénès | 2018-06-01 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7660: Add codeowner for timing python scripts | Maxime Dénès | 2018-06-01 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | * | | | | | | | | | | | | | | | | | | | | | | | | | | Merge two clearbody docs | Théo Winterhalter | 2018-06-01 | |
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7652: Explicitly require python2 in python scripts in tools/ | Jason Gross | 2018-05-31 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Add codeowner for timing python scripts | Jason Gross | 2018-05-31 | |
| |/ / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fix a couple typos in deprecation messages | Armaël Guéneau | 2018-05-31 | |
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7401: Automatically run alienclean before compiling. | Enrico Tassi | 2018-05-31 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Explicitly require python2 in python scripts in tools/ | Armaël Guéneau | 2018-05-31 | |
| |/ / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Remove some dead code in class_tactics.ml | Armaël Guéneau | 2018-05-31 | |
| |_|_|_|_|_|/ / / / / / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | | | | * | | | | | | | | | | | | | Refactor parsing rules for Hint Resolve -> and Hint Resolve <- | Armaël Guéneau | 2018-05-31 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [notations] Split interpretation and parsing of notations | Emilio Jesus Gallego Arias | 2018-05-31 | |
| | | | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [api] Move `Constrexpr` to the `interp` module. | Emilio Jesus Gallego Arias | 2018-05-31 | |
| |_|_|/ / / / / / / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #6969: [api] Remove functions deprecated in 8.8 | Maxime Dénès | 2018-05-31 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | * | | | | | | | | | | | | | | | | | | | | | | | | | Indicate in the doc that clearbody can take several idents | Théo Winterhalter | 2018-05-31 | |
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7564: Move interning the [hint_pattern] outside the Typeclasses hooks. | Emilio Jesus Gallego Arias | 2018-05-31 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | | | | | | | | * | | | | | | | | Fix #4714: Stack overflow with native compute | Maxime Dénès | 2018-05-31 | |
| | | | | | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | Reduce circular dependency constants <-> projections | Gaëtan Gilbert | 2018-05-31 | |
| |_|_|_|_|/ / / / / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7578: Allow make clean to work on a fresh clone | Enrico Tassi | 2018-05-31 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7639: Makefile: fix undefined NATIVEFILES when -native-compute no | Enrico Tassi | 2018-05-31 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7633: [Makefile] New target “install-merlin” | Enrico Tassi | 2018-05-31 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Move interning the [hint_pattern] outside the Typeclasses hooks. | Gaëtan Gilbert | 2018-05-30 | |
| |_|_|/ / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [api] Remove deprecated objects in engine / interp / library | Emilio Jesus Gallego Arias | 2018-05-30 | |
| | | | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [api] Remove deprecated object from `Term` | Emilio Jesus Gallego Arias | 2018-05-30 | |
| | | | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [api] Remove deprecated aliases from `Names`. | Emilio Jesus Gallego Arias | 2018-05-30 | |
| | | | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [api] Reintroduce `Names.global_reference` alias | Emilio Jesus Gallego Arias | 2018-05-30 | |
| |_|_|/ / / / / / / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7260: Fix #6951: Unexpected error during scheme creation. | Maxime Dénès | 2018-05-30 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7558: [api] Make `vernac/` self-contained. | Maxime Dénès | 2018-05-30 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |