Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge PR #7349: Fix an anomaly when calling Obligation 0 or Obligation -1. | 2018-06-04 | |
|\ | |||
* \ | Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ta... | 2018-06-04 | |
|\ \ | |||
* \ \ | Merge PR #7216: Replace uses of Termops.dependent by more specific functions. | 2018-06-04 | |
|\ \ \ | |||
* \ \ \ | Merge PR #7552: Fix #7539: Checker does not properly handle negative coinduct... | 2018-06-04 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found". | 2018-06-04 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #7249: Cleaning, documentation, uniformisation of the Coq extension ... | 2018-06-04 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #7619: Mention test-suite in PR template | 2018-06-04 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #7648: Indicate in the doc that clearbody can take several idents | 2018-06-04 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel. | 2018-06-04 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #7657: Fix a couple typos in deprecation messages | 2018-06-04 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #7640: Small refactoring to clarify make_local_hint_db. | 2018-06-04 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7649: Remove some dead code in class_tactics.ml | 2018-06-04 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7682: Fixes #7641: more detailed message about disjunctive patterns... | 2018-06-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | 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 | |
| |/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | |||
| * | | | | | | | | | | | | | [ci] Expose updated `OCAMLPATH` for CI users. | 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 | |
| |_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | |||
| | | | * | | | | | | | | | | | | [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 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | |||
| | | | | | * | | | | | | | | | | 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 | |
| |_|_|/ / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | |