Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix the wrapper around ocamldebug. | 2018-01-15 | |
| | | | | | Since 5ffa147, there is a new clib folder that needed to be added to the set of includes of ocamldebug | ||
* | Merge PR #6483: Strong invariants in polymorphic definitions | 2018-01-12 | |
|\ | |||
| * | Adding a custom Travis overlay for HoTT. | 2018-01-11 | |
| | | |||
* | | Merge PR #6557: First stab at documenting the test suite. | 2018-01-11 | |
|\ \ | |||
* \ \ | Merge PR #6519: Python script checking missing/unnecessary [needs: rebase] label | 2018-01-10 | |
|\ \ \ | |_|/ |/| | | |||
* | | | Merge PR #6549: Normalize package names | 2018-01-08 | |
|\ \ \ | |||
* \ \ \ | Merge PR #6527: Update backport script for more control. | 2018-01-08 | |
|\ \ \ \ | |||
| | | * | | github-check-prs.py: print PR URLs when needed. | 2018-01-08 | |
| | | | | | |||
| | | * | | github-check-prs.py: Strip spaces from token from command line | 2018-01-08 | |
| | | | | | |||
| | | * | | github-check-prs.py: command line option to get token from a file | 2018-01-08 | |
| | | | | | |||
* | | | | | Merge PR #6501: Document use of ocamldebug from the command line in ↵ | 2018-01-08 | |
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | | Cygwin/Windows | ||
| | | | | * | First stab at documenting the test suite. | 2018-01-06 | |
| |_|_|_|/ |/| | | | | |||
| | | * | | Normalize MacOS installer name. | 2018-01-04 | |
| | | | | | |||
| | | * | | Normalize Windows installer names. | 2018-01-04 | |
| |_|/ / |/| | | | |||
| | | * | Expound on dependencies for github-check-prs.py | 2017-12-30 | |
| | | | | |||
| | | * | Python script checking missing/unnecessary [needs: rebase] label | 2017-12-30 | |
| | | | | |||
| * | | | Add instructions for debugging from the command line (and in Windows) | 2017-12-29 | |
| | | | | | | | | | | | | | | | | Avoid generating \r characters in generated dev/ocamldebug-coq (affects Windows) | ||
* | | | | Merge PR #6493: [API] remove large file containing duplicate interfaces | 2017-12-29 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6405: Remove the local polymorphic flag hack. | 2017-12-29 | |
|\ \ \ \ \ | |_|_|_|/ |/| | | | | |||
| | * | | | overlay for #6493 | 2017-12-27 | |
| | | | | | |||
| | * | | | [API] remove large file containing duplicate interfaces | 2017-12-27 | |
| |/ / / |/| | | | | | | | | | | | | | | | ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client. | ||
* | | | | Merge PR #6102: Fix #5998: AppVeyor package building is currently failing | 2017-12-27 | |
|\ \ \ \ | |||
| | * | | | Add equations overlay. | 2017-12-27 | |
| |/ / / |/| | | | |||
| * | | | Fix #5998: AppVeyor package building is currently failing | 2017-12-27 | |
| | | | | |||
* | | | | Merge PR #6507: [ide] [doc] Document tweak to Query call. | 2017-12-27 | |
|\ \ \ \ | |||
| * | | | | [ide] [doc] Document tweak to Query call. | 2017-12-26 | |
| | |/ / | |/| | | |||
* | | | | Fix overlay selection for Circle CI. | 2017-12-26 | |
| | | | | |||
* | | | | Delete old overlays (leaving example) | 2017-12-26 | |
|/ / / | |||
| | * | Update backport script for more control. | 2017-12-24 | |
| |/ |/| | |||
* | | Merge PR #6318: Separate vernac controls and regular commands. | 2017-12-22 | |
|\ \ | |||
* | | | Fix CI with parallel make (messed up dependencies) | 2017-12-21 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | When invoking through Makefile we always rebuild dependencies. To skip dependencies, invoke ci-wrapper directly. We make Circle CI do this. In order to properly support invoking ci-wrapper directly we replace "make" in ci-common by a bash function which adds -j to the make invocation outside submakes. We also set TIMED in the ci-wrapper. | ||
| * | | Separate vernac controls and regular commands. | 2017-12-20 | |
|/ / | | | | | | | | | | | | | | | | | | | | | | | Virtually all classifications of vernacular commands (the STM classifier, "filtered commands", "navigation commands", etc.) were broken in presence of control vernaculars like Time, Timeout, Fail. Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac Debug in CoqIDE. This change introduces a type separation between vernacular controls and vernacular commands, together with an "under_control" combinator. | ||
* | | Merge PR #6400: Circle CI | 2017-12-19 | |
|\ \ | |||
* \ \ | Merge PR #6305: Build with windows line endings | 2017-12-18 | |
|\ \ \ | |||
* \ \ \ | Merge PR #6217: Do dependencies in 1 command per file class. | 2017-12-18 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6419: [vernac] Split `command.ml` into separate files. | 2017-12-18 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6413: [econstr] Switch constrintern API to non-imperative style. | 2017-12-18 | |
|\ \ \ \ \ \ | |||
| | * | | | | | [vernac] Split `command.ml` into separate files. | 2017-12-17 | |
| |/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Over the time, `Command` grew organically and it has become now one of the most complex files in the codebase; however, its functionality is well separated into 4 key components that have little to do with each other. We thus split the file, and also document the interfaces. Some parts of `Command` export tricky internals to use by other plugins, and it is common that plugin writers tend to get confused, so we are more explicit about these parts now. This patch depends on #6413. | ||
| | | * | | | Fix build file | 2017-12-16 | |
| | | | | | | |||
| | * | | | | Overlay for unimath. | 2017-12-15 | |
| | | | | | | |||
* | | | | | | Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml` | 2017-12-15 | |
|\ \ \ \ \ \ | |_|_|_|_|/ |/| | | | | | |||
| | * | | | | [econstr] Switch constrintern API to non-imperative style. | 2017-12-15 | |
| |/ / / / | | | | | | | | | | | | | | | | | | | | | We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step desirable to progress with EConstr there. | ||
* | | | | | Merge PR #6169: Clean up/deprecated options | 2017-12-14 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind. | 2017-12-14 | |
|\ \ \ \ \ \ | |||
| | | | | | * | Put bignums, math-classes and corn dependencies in Makefile | 2017-12-13 | |
| | | | | | | | |||
| | | * | | | | [econstr] Cleanup in `vernac/classes.ml`. | 2017-12-13 | |
| | | | |/ / | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We fix quite a few types, and perform some cleanup wrt to the evar_map, in particular we prefer to thread it now as otherwise it may become trickier to check when we are using the correct one. Thanks to @SkySkimmer for lots of comments and bug-finding. | ||
* | | / | | | Revert "[ci] Temporal workaround for checker non-backwards compatible change." | 2017-12-12 | |
| |_|/ / / |/| | | | | | | | | | | | | | | This reverts commit 5d4cf69a3d7d472b54b5decc8400164b87e9a73f. | ||
* | | | | | Merge PR #6331: Linter: skip PRs older than the linter. | 2017-12-11 | |
|\ \ \ \ \ | |_|_|_|/ |/| | | | | |||
| | | * | | Add overlay. | 2017-12-11 | |
| |_|/ / |/| | | | |||
* | | | | Merge PR #6368: [api] Remove yet another type alias. | 2017-12-11 | |
|\ \ \ \ |