aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2018-01-08Merge PR #6527: Update backport script for more control.Maxime Dénès
2018-01-08Merge PR #6501: Document use of ocamldebug from the command line in ↵Maxime Dénès
Cygwin/Windows
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
2017-12-11Merge PR #6346: [ci] CoLoR has moved to githubMaxime Dénès
2017-12-10[build] Remove coqmktop in favor of ocamlfind.Emilio Jesus Gallego Arias
We remove coqmktop in favor of a couple of simple makefile rules using ocamlfind. In order to do that, we introduce a new top-level file that calls the coqtop main entry. This is very convenient in order to use other builds systems such as `ocamlbuild` or `jbuilder`. An additional consideration is that we must perform a side-effect on init depending on whether we have an OCaml toplevel available [byte] or not. We do that by using two different object files, one for the bytecode version other for the native one, but we may want to review our choice. We also perform some smaller cleanups taking profit from ocamlfind.
2017-12-10[ci] Temporal workaround for checker non-backwards compatible change.Emilio Jesus Gallego Arias
2017-12-09[api] Remove yet another type alias.Emilio Jesus Gallego Arias
2017-12-09[lib] Rename Profile to CProfileEmilio Jesus Gallego Arias
New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
2017-12-09[ci] Download ci-sf archives into the proper CI build dir.Emilio Jesus Gallego Arias
Currently, `make ci-sf` downloads and builds the files in the main root directory. we fix that.
2017-12-08Fix a copy-paste error in ci-ltac2.Théo Zimmermann
2017-12-08Merge PR #6158: Allows a level in the raw and glob printersMaxime Dénès
2017-12-07[ci] CoLoR has moved to githubEmilio Jesus Gallego Arias
Closes #6194 .
2017-12-07Merge PR #6267: Fix PR merge script.Maxime Dénès
2017-12-06Overlay for Equations.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 07:45:06 +0000