| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-12-21 | Fix 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-20 | Separate 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-19 | Merge PR #6400: Circle CI | Maxime Dénès | |
| 2017-12-18 | Merge PR #6305: Build with windows line endings | Maxime Dénès | |
| 2017-12-18 | Merge PR #6217: Do dependencies in 1 command per file class. | Maxime Dénès | |
| 2017-12-18 | Merge PR #6419: [vernac] Split `command.ml` into separate files. | Maxime Dénès | |
| 2017-12-18 | Merge 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-16 | Fix build file | Jim | |
| 2017-12-15 | Overlay for unimath. | Gaëtan Gilbert | |
| 2017-12-15 | Merge 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-14 | Merge PR #6169: Clean up/deprecated options | Maxime Dénès | |
| 2017-12-14 | Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind. | Maxime Dénès | |
| 2017-12-13 | Put bignums, math-classes and corn dependencies in Makefile | Gaë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-12 | Revert "[ci] Temporal workaround for checker non-backwards compatible change." | Théo Zimmermann | |
| This reverts commit 5d4cf69a3d7d472b54b5decc8400164b87e9a73f. | |||
| 2017-12-11 | Merge PR #6331: Linter: skip PRs older than the linter. | Maxime Dénès | |
| 2017-12-11 | Add overlay. | Théo Zimmermann | |
| 2017-12-11 | Merge PR #6368: [api] Remove yet another type alias. | Maxime Dénès | |
| 2017-12-11 | Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract. | Maxime Dénès | |
| 2017-12-11 | Merge PR #6358: [ci] Download ci-sf archives into the proper CI build dir. | Maxime Dénès | |
| 2017-12-11 | Merge PR #6351: Fix a copy-paste error in ci-ltac2. | Maxime Dénès | |
| 2017-12-11 | Merge PR #6346: [ci] CoLoR has moved to github | Maxime 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 CProfile | Emilio 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-08 | Fix a copy-paste error in ci-ltac2. | Théo Zimmermann | |
| 2017-12-08 | Merge PR #6158: Allows a level in the raw and glob printers | Maxime Dénès | |
| 2017-12-07 | [ci] CoLoR has moved to github | Emilio Jesus Gallego Arias | |
| Closes #6194 . | |||
| 2017-12-07 | Merge PR #6267: Fix PR merge script. | Maxime Dénès | |
| 2017-12-06 | Overlay for Equations. | Gaëtan Gilbert | |
| 2017-12-06 | Linter: skip PRs older than the linter. | Gaëtan Gilbert | |
| 2017-12-01 | uninstall doc dir, not dev (which is not installed), #6007 | Paul Steckler | |
| 2017-12-01 | Merge PR #736: [ci] Test coqchk on the CompCert target. | Maxime Dénès | |
| 2017-11-30 | Merge PR #6244: [lib] [api] Introduce record for `object_prefix` | Maxime Dénès | |
| 2017-11-30 | [ci] Test coqchk on the CompCert target. | Théo Zimmermann | |
| 2017-11-30 | Merge PR #6269: [ci] [vst] Shorten compilation time to avoid Travis timeouts. | Maxime Dénès | |
| 2017-11-29 | Fix usage comment. | Théo Zimmermann | |
| 2017-11-29 | This script apparently uses bash-specific features. | Théo Zimmermann | |
| 2017-11-29 | Fix PR merge script. | Théo Zimmermann | |
| Was still relying on the existence of user-configured /pr/. | |||
| 2017-11-29 | [lib] [api] Introduce record for `object_prefix` | Emilio Jesus Gallego Arias | |
| This is a minor cleanup adding a record in a try to structure the state living in `Lib`. | |||
| 2017-11-28 | Add PR backport script. | Théo Zimmermann | |
| 2017-11-28 | [ci] [vst] Shorten compilation time to avoid Travis timeouts. | Emilio Jesus Gallego Arias | |
| We remove the progs target [examples] to save time, we still build the full library thou. I guess we can't do better for now unless we get some Travis subscription. | |||
| 2017-11-28 | Merge PR #6259: Add PR merge script. | Maxime Dénès | |
| 2017-11-28 | Add PR merge script. | Maxime Dénès | |
| 2017-11-28 | Merge PR #1033: Universe binder improvements | Maxime Dénès | |
| 2017-11-28 | Merge PR #6248: [api] Remove aliases of `Evar.t` | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |