aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2018-01-11Merge PR #6557: First stab at documenting the test suite.Maxime Dénès
2018-01-10Merge PR #6519: Python script checking missing/unnecessary [needs: rebase] labelMaxime Dénès
2018-01-08Merge PR #6549: Normalize package namesMaxime Dénès
2018-01-08Merge PR #6527: Update backport script for more control.Maxime Dénès
2018-01-08github-check-prs.py: print PR URLs when needed.Gaëtan Gilbert
2018-01-08github-check-prs.py: Strip spaces from token from command lineGaëtan Gilbert
2018-01-08github-check-prs.py: command line option to get token from a fileGaëtan Gilbert
2018-01-08Merge PR #6501: Document use of ocamldebug from the command line in ↵Maxime Dénès
Cygwin/Windows
2018-01-06First stab at documenting the test suite.Jasper Hugunin
2018-01-04Normalize MacOS installer name.Théo Zimmermann
2018-01-04Normalize Windows installer names.Théo Zimmermann
2017-12-30Expound on dependencies for github-check-prs.pyGaëtan Gilbert
2017-12-30Python script checking missing/unnecessary [needs: rebase] labelGaëtan Gilbert
2017-12-29Add instructions for debugging from the command line (and in Windows)Jim Fehrle
Avoid generating \r characters in generated dev/ocamldebug-coq (affects Windows)
2017-12-29Merge PR #6493: [API] remove large file containing duplicate interfacesMaxime Dénès
2017-12-29Merge PR #6405: Remove the local polymorphic flag hack.Maxime Dénès
2017-12-27overlay for #6493Enrico Tassi
2017-12-27[API] remove large file containing duplicate interfacesEnrico Tassi
... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
2017-12-27Merge PR #6102: Fix #5998: AppVeyor package building is currently failingMaxime Dénès
2017-12-27Add equations overlay.Maxime Dénès
2017-12-27Fix #5998: AppVeyor package building is currently failingMaxime Dénès
2017-12-27Merge PR #6507: [ide] [doc] Document tweak to Query call.Maxime Dénès
2017-12-26[ide] [doc] Document tweak to Query call.Emilio Jesus Gallego Arias
2017-12-26Fix overlay selection for Circle CI.Gaëtan Gilbert
2017-12-26Delete old overlays (leaving example)Gaëtan Gilbert
2017-12-24Update backport script for more control.Théo Zimmermann
2017-12-22Merge PR #6318: Separate vernac controls and regular commands.Maxime Dénès
2017-12-21Fix CI with parallel make (messed up dependencies)Gaëtan Gilbert
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.
2017-12-20Separate vernac controls and regular commands.Maxime Dénès
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.
2017-12-19Merge PR #6400: Circle CIMaxime Dénès
2017-12-18Merge PR #6305: Build with windows line endingsMaxime Dénès
2017-12-18Merge PR #6217: Do dependencies in 1 command per file class.Maxime Dénès
2017-12-18Merge PR #6419: [vernac] Split `command.ml` into separate files.Maxime Dénès
2017-12-18Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Maxime Dénès
2017-12-17[vernac] Split `command.ml` into separate files.Emilio Jesus Gallego Arias
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.
2017-12-16Fix build fileJim
2017-12-15Overlay for unimath.Gaëtan Gilbert
2017-12-15Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`Maxime Dénès
2017-12-15[econstr] Switch constrintern API to non-imperative style.Emilio Jesus Gallego Arias
We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step desirable to progress with EConstr there.
2017-12-14Merge PR #6169: Clean up/deprecated optionsMaxime Dénès
2017-12-14Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Maxime Dénès
2017-12-13Put bignums, math-classes and corn dependencies in MakefileGaëtan Gilbert
2017-12-13[econstr] Cleanup in `vernac/classes.ml`.Emilio Jesus Gallego Arias
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.
2017-12-12Revert "[ci] Temporal workaround for checker non-backwards compatible change."Théo Zimmermann
This reverts commit 5d4cf69a3d7d472b54b5decc8400164b87e9a73f.
2017-12-11Merge PR #6331: Linter: skip PRs older than the linter.Maxime Dénès
2017-12-11Add overlay.Théo Zimmermann
2017-12-11Merge PR #6368: [api] Remove yet another type alias.Maxime Dénès
2017-12-11Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Maxime Dénès
2017-12-11Merge PR #6358: [ci] Download ci-sf archives into the proper CI build dir.Maxime Dénès
2017-12-11Merge PR #6351: Fix a copy-paste error in ci-ltac2.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 12:09:29 +0000