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