aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* Merge PR #6405: Remove the local polymorphic flag hack.Gravatar Maxime Dénès2017-12-29
|\
* \ Merge PR #6102: Fix #5998: AppVeyor package building is currently failingGravatar Maxime Dénès2017-12-27
|\ \
| | * Add equations overlay.Gravatar Maxime Dénès2017-12-27
| |/ |/|
| * Fix #5998: AppVeyor package building is currently failingGravatar Maxime Dénès2017-12-27
| |
* | Merge PR #6507: [ide] [doc] Document tweak to Query call.Gravatar Maxime Dénès2017-12-27
|\ \
| * | [ide] [doc] Document tweak to Query call.Gravatar Emilio Jesus Gallego Arias2017-12-26
| | |
* | | Fix overlay selection for Circle CI.Gravatar Gaëtan Gilbert2017-12-26
| | |
* | | Delete old overlays (leaving example)Gravatar Gaëtan Gilbert2017-12-26
|/ /
* | Merge PR #6318: Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-22
|\ \
* | | Fix CI with parallel make (messed up dependencies)Gravatar Gaëtan Gilbert2017-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.Gravatar Maxime Dénès2017-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 CIGravatar Maxime Dénès2017-12-19
|\ \
* \ \ Merge PR #6305: Build with windows line endingsGravatar Maxime Dénès2017-12-18
|\ \ \
* \ \ \ Merge PR #6217: Do dependencies in 1 command per file class.Gravatar Maxime Dénès2017-12-18
|\ \ \ \
* \ \ \ \ Merge PR #6419: [vernac] Split `command.ml` into separate files.Gravatar Maxime Dénès2017-12-18
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Gravatar Maxime Dénès2017-12-18
|\ \ \ \ \ \
| | * | | | | [vernac] Split `command.ml` into separate files.Gravatar Emilio Jesus Gallego Arias2017-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 fileGravatar Jim2017-12-16
| | | | | |
| | * | | | Overlay for unimath.Gravatar Gaëtan Gilbert2017-12-15
| | | | | |
* | | | | | Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`Gravatar Maxime Dénès2017-12-15
|\ \ \ \ \ \ | |_|_|_|_|/ |/| | | | |
| | * | | | [econstr] Switch constrintern API to non-imperative style.Gravatar Emilio Jesus Gallego Arias2017-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 optionsGravatar Maxime Dénès2017-12-14
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\ \ \ \ \ \
| | | | | | * Put bignums, math-classes and corn dependencies in MakefileGravatar Gaëtan Gilbert2017-12-13
| | | | | | |
| | | * | | | [econstr] Cleanup in `vernac/classes.ml`.Gravatar Emilio Jesus Gallego Arias2017-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."Gravatar Théo Zimmermann2017-12-12
| |_|/ / / |/| | | | | | | | | | | | | | This reverts commit 5d4cf69a3d7d472b54b5decc8400164b87e9a73f.
* | | | | Merge PR #6331: Linter: skip PRs older than the linter.Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \ | |_|_|_|/ |/| | | |
| | | * | Add overlay.Gravatar Théo Zimmermann2017-12-11
| |_|/ / |/| | |
* | | | Merge PR #6368: [api] Remove yet another type alias.Gravatar Maxime Dénès2017-12-11
|\ \ \ \
* \ \ \ \ Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6358: [ci] Download ci-sf archives into the proper CI build dir.Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6351: Fix a copy-paste error in ci-ltac2.Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6346: [ci] CoLoR has moved to githubGravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \ \ \
| | | | | | | * | [build] Remove coqmktop in favor of ocamlfind.Gravatar Emilio Jesus Gallego Arias2017-12-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | | | | [ci] Temporal workaround for checker non-backwards compatible change.Gravatar Emilio Jesus Gallego Arias2017-12-10
| | | | | | | | |
| | | | | * | | | [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
| |_|_|_|/ / / / |/| | | | | | |
| | | | | | * | [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
| |_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
| | | * | | | [ci] Download ci-sf archives into the proper CI build dir.Gravatar Emilio Jesus Gallego Arias2017-12-09
| |_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | Currently, `make ci-sf` downloads and builds the files in the main root directory. we fix that.
| | * | | | Fix a copy-paste error in ci-ltac2.Gravatar Théo Zimmermann2017-12-08
| | | | | |
* | | | | | Merge PR #6158: Allows a level in the raw and glob printersGravatar Maxime Dénès2017-12-08
|\ \ \ \ \ \
| | * | | | | [ci] CoLoR has moved to githubGravatar Emilio Jesus Gallego Arias2017-12-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Closes #6194 .
* | | | | | | Merge PR #6267: Fix PR merge script.Gravatar Maxime Dénès2017-12-07
|\ \ \ \ \ \ \ | |_|/ / / / / |/| | | | | |
| | | | * | | Overlay for Equations.Gravatar Gaëtan Gilbert2017-12-06
| |_|_|/ / / |/| | | | |
| | | | * | Linter: skip PRs older than the linter.Gravatar Gaëtan Gilbert2017-12-06
| |_|_|/ / |/| | | |
* | | | | uninstall doc dir, not dev (which is not installed), #6007Gravatar Paul Steckler2017-12-01
| | | | |
* | | | | Merge PR #736: [ci] Test coqchk on the CompCert target.Gravatar Maxime Dénès2017-12-01
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6244: [lib] [api] Introduce record for `object_prefix`Gravatar Maxime Dénès2017-11-30
|\ \ \ \ \ \
| | * | | | | [ci] Test coqchk on the CompCert target.Gravatar Théo Zimmermann2017-11-30
| |/ / / / / |/| | | | |
* | | | | | Merge PR #6269: [ci] [vst] Shorten compilation time to avoid Travis timeouts.Gravatar Maxime Dénès2017-11-30
|\ \ \ \ \ \
| | | * | | | Fix usage comment.Gravatar Théo Zimmermann2017-11-29
| | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 16:52:49 +0000