Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | | | | | | | | | | | Merge PR #6533: Update the lower-bound of the lablgtk dependency. | Maxime Dénès | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6425: Cleanup universes in the kernel | Maxime Dénès | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6516: Add TIMING_SORT_BY and --sort-by to timing scripts | Maxime Dénès | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6530: Ignore generated test-suite/output/MExtraction.out | Maxime Dénès | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6517: Trim more trailing whitespace in coq-makefile timing test | Maxime Dénès | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6527: Update backport script for more control. | Maxime Dénès | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6526: Fixing various typos in the Credits chapter. | Maxime Dénès | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | * | | | | | | | | github-check-prs.py: print PR URLs when needed. | Gaëtan Gilbert | 2018-01-08 | |
| | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | * | | | | | | | | github-check-prs.py: Strip spaces from token from command line | Gaëtan Gilbert | 2018-01-08 | |
| | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | * | | | | | | | | github-check-prs.py: command line option to get token from a file | Gaëtan Gilbert | 2018-01-08 | |
| | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | Merge PR #6510: Document between and exists_between types. | Maxime Dénès | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | | | | | | | | | | | | Document between and exists_between types. | Ismail | 2018-01-08 | |
| | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | Merge PR #6518: Fix build of micromega & nsatz with OCaml 4.06 | Maxime Dénès | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6501: Document use of ocamldebug from the command line in ↵ | Maxime Dénès | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Cygwin/Windows | |||
| | | | | | | | | | | | | | | | | * | | | | | | Mention -B argument of make to rerun tests | Jasper Hugunin | 2018-01-07 | |
| | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | * | | | | | | First stab at documenting the test suite. | Jasper Hugunin | 2018-01-06 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | * | | | | | | [PR template] Remove the relative link. | Théo Zimmermann | 2018-01-05 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was actually pointing to https://github.com/CHANGES. | |||
| | | | | | | | | | | | | | | | * | | | | | Documentation and CHANGES for bracket with goal selector. | Théo Zimmermann | 2018-01-05 | |
| | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | * | | | | | Brackets support single numbered goal selectors. | Théo Zimmermann | 2018-01-05 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows to focus on a sub-goal other than the first one without resorting to the `Focus` command. | |||
| | | | | | | | | | | * | | | | | | | | | Normalize MacOS installer name. | Théo Zimmermann | 2018-01-04 | |
| | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | * | | | | | | | | | Normalize Windows installer names. | Théo Zimmermann | 2018-01-04 | |
| |_|_|_|_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | * | | | | | | | | | Update the lower-bound of the lablgtk dependency. | Théo Zimmermann | 2018-01-04 | |
| |_|_|_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Closes #6509. | |||
| | | | | | | | | | * | | | | | | | | add optimize_heap tactic for #6488 | Paul Steckler | 2018-01-03 | |
| | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | * | | | | | | | update PNGs; mention async error handling; change query window to query ↵ | Paul Steckler | 2018-01-03 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | pane; use color descriptions | |||
| | | | | | | | | | | | * | | | | | | Fix mli-doc issue #6531 | Tony Beta Lambda | 2018-01-01 | |
| |_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | ||||
| | | | | | | * | | | | | | | | | | Ignore generated test-suite/output/MExtraction.out | Jason Gross | 2017-12-31 | |
| |_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | ||||
| | | | | | * | | | | | | | | | | Trim more trailing whitespace in coq-makefile timing test | Jason Gross | 2017-12-31 | |
| |_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Should help with https://github.com/coq/coq/issues/5675#issuecomment-353604702 Also replace a tab with spaces | |||
| | | | | | | * | | | | | | | | Add a comment about universe lifting in sections in the kernel. | Pierre-Marie Pédrot | 2017-12-31 | |
| | | | | | | | | | | | | | | | ||||
| | | | | | | | | | * | | | | | Expound on dependencies for github-check-prs.py | Gaëtan Gilbert | 2017-12-30 | |
| | | | | | | | | | | | | | | | ||||
| | | | | | | | | | * | | | | | Python script checking missing/unnecessary [needs: rebase] label | Gaëtan Gilbert | 2017-12-30 | |
| | | | |_|_|_|_|_|/ / / / / | | | |/| | | | | | | | | | | ||||
| | | | | | | * | | | | | | | Moving some universe substitution code out of the kernel. | Pierre-Marie Pédrot | 2017-12-30 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This code was not used at all inside the kernel, it was related to universe unification that happens in the upper layer. It makes more sense to put it somewhere upper. | |||
| | | | | | | * | | | | | | | Returning instance instead of substitution in universe context abstraction. | Pierre-Marie Pédrot | 2017-12-30 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This datatype enforces stronger invariants, e.g. that we only have in the substitution codomain a connex interval of variables from 0 to n - 1. | |||
| | | | | | | * | | | | | | | Hardening universe abstraction in Cooking. | Pierre-Marie Pédrot | 2017-12-30 | |
| | | | | | | | | | | | | | | ||||
| | | | | | | * | | | | | | | Using a dedicated type for Lib.abstr_info. | Pierre-Marie Pédrot | 2017-12-30 | |
| |_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | Add instructions for debugging from the command line (and in Windows) | Jim Fehrle | 2017-12-29 | |
| | |_|_|_|_|/ / / / / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Avoid generating \r characters in generated dev/ocamldebug-coq (affects Windows) | |||
| | | | | | | | | * | | | [vernac] adds the “program” flag to the “atts” record | Vincent Laporte | 2017-12-29 | |
| | | | | | | | | | | | | ||||
| | | | | | | | | * | | | [vernac] Define types in order | Vincent Laporte | 2017-12-29 | |
| |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | ||||
* | | | | | | | | | | | Merge PR #6493: [API] remove large file containing duplicate interfaces | Maxime Dénès | 2017-12-29 | |
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #975: Create checklist for pull requests. | Maxime Dénès | 2017-12-29 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6492: Remove query-in-IDE warning. | Maxime Dénès | 2017-12-29 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6405: Remove the local polymorphic flag hack. | Maxime Dénès | 2017-12-29 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6433: [flags] Move global time flag into an attribute. | Maxime Dénès | 2017-12-29 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | ||||
| | | | | | | * | | | | | | | | [Makefile] plugins micromega and nsatz depend on unix and num | Vincent Laporte | 2017-12-28 | |
| | | | | | | | | | | | | | | | ||||
| | | | | | | * | | | | | | | | [default.nix] depends on ocamlPackages.num | Vincent Laporte | 2017-12-28 | |
| |_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | ||||
| | | | | | | | | * | | | | | Add TIMING_SORT_BY and --sort-by to timing scripts | Jason Gross | 2017-12-27 | |
| |_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This should help with #5675, in particular with https://github.com/coq/coq/issues/5675#issuecomment-349716292 | |||
| | | | | * | | | | | | | | overlay for #6493 | Enrico Tassi | 2017-12-27 | |
| | | | | | | | | | | | | | ||||
| | | | | * | | | | | | | | [API] remove large file containing duplicate interfaces | Enrico Tassi | 2017-12-27 | |
| |_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client. | |||
| | | * | | | | | | | | | Remove query-in-IDE warning. | Maxime Dénès | 2017-12-27 | |
| |_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I don't understand what is wrong with putting a query in a script running in the IDE. It is typically needed when giving demos, and that sounds like a ligitimate use case. By the way, we do it ourselves every year during the demo at CoqPL... | |||
* | | | | | | | | | | | Merge PR #6102: Fix #5998: AppVeyor package building is currently failing | Maxime Dénès | 2017-12-27 | |
|\ \ \ \ \ \ \ \ \ \ \ | ||||
| | | * | | | | | | | | | Add equations overlay. | Maxime Dénès | 2017-12-27 | |
| | | | | | | | | | | | |