Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #6610: Points to Flocq official repository. | Maxime Dénès | 2018-02-07 |
|\ | |||
* \ | Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding | Maxime Dénès | 2018-02-07 |
|\ \ | |||
| | * | Points to Flocq official repository. | Théo Zimmermann | 2018-02-05 |
| |/ |/| | | | | | Following comment at https://github.com/coq/coq/pull/6596#issuecomment-358246528. | ||
| * | Add overlay for equations (nf_beta takes an env) | Gaëtan Gilbert | 2018-02-05 |
| | | |||
* | | Merge PR #6654: CI: Run coqchk on Iris | Maxime Dénès | 2018-02-05 |
|\ \ | |/ |/| | |||
| * | CI: Run coqchk on Iris | Ralf Jung | 2018-01-31 |
| | | |||
* | | Merge PR #6641: ci-compcert.sh: use default value for NJOBS when installing ↵ | Maxime Dénès | 2018-01-31 |
|\ \ | | | | | | | | | | menhir. | ||
* \ \ | Merge PR #6535: Cleanup name-binding structure for fresh evar name generation. | Maxime Dénès | 2018-01-31 |
|\ \ \ | |_|/ |/| | | |||
| | * | Put default value for NJOBS in ci-common. | Gaëtan Gilbert | 2018-01-30 |
| |/ |/| | |||
| * | Adding an overlay for Equations. | Pierre-Marie Pédrot | 2018-01-30 |
| | | |||
* | | Merge PR #6568: Cleanup scripts | Maxime Dénès | 2018-01-23 |
|\ \ | |||
| * | | Source basic overlay before user overlays. | Gaëtan Gilbert | 2018-01-16 |
| | | | |||
| * | | Cleanup shell expansions and quoting. | Gaëtan Gilbert | 2018-01-16 |
| |/ | |||
* | | Merge PR #6483: Strong invariants in polymorphic definitions | Maxime Dénès | 2018-01-12 |
|\ \ | |||
| * | | Adding a custom Travis overlay for HoTT. | Pierre-Marie Pédrot | 2018-01-11 |
| | | | |||
* | | | Merge PR #6557: First stab at documenting the test suite. | Maxime Dénès | 2018-01-11 |
|\ \ \ | |/ / |/| | | |||
| * | | First stab at documenting the test suite. | Jasper Hugunin | 2018-01-06 |
| |/ | |||
* / | Normalize Windows installer names. | Théo Zimmermann | 2018-01-04 |
|/ | |||
* | Merge PR #6493: [API] remove large file containing duplicate interfaces | Maxime Dénès | 2017-12-29 |
|\ | |||
* \ | Merge PR #6405: Remove the local polymorphic flag hack. | Maxime Dénès | 2017-12-29 |
|\ \ | |||
| | * | overlay for #6493 | Enrico Tassi | 2017-12-27 |
| |/ |/| | |||
* | | Merge PR #6102: Fix #5998: AppVeyor package building is currently failing | Maxime Dénès | 2017-12-27 |
|\ \ | |||
| | * | Add equations overlay. | Maxime Dénès | 2017-12-27 |
| |/ |/| | |||
| * | Fix #5998: AppVeyor package building is currently failing | Maxime Dénès | 2017-12-27 |
| | | |||
* | | Fix overlay selection for Circle CI. | Gaëtan Gilbert | 2017-12-26 |
| | | |||
* | | Delete old overlays (leaving example) | Gaëtan Gilbert | 2017-12-26 |
| | | |||
* | | Fix CI with parallel make (messed up dependencies) | Gaëtan Gilbert | 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. | ||
* | | Merge PR #6400: Circle CI | Maxime Dénès | 2017-12-19 |
|\ \ | |||
* \ \ | Merge PR #6217: Do dependencies in 1 command per file class. | Maxime Dénès | 2017-12-18 |
|\ \ \ | |||
* \ \ \ | Merge PR #6413: [econstr] Switch constrintern API to non-imperative style. | Maxime Dénès | 2017-12-18 |
|\ \ \ \ | |||
| | * | | | 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 | 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 | Maxime Dénès | 2017-12-14 |
|\ \ \ \ | |||
| | | | * | 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 | 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." | Théo Zimmermann | 2017-12-12 |
| |/ / |/| | | | | | | | | This reverts commit 5d4cf69a3d7d472b54b5decc8400164b87e9a73f. | ||
| * | | Add overlay. | Théo Zimmermann | 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-11 |
|\ \ \ \ \ | |||
* | | | | | | [ci] Temporal workaround for checker non-backwards compatible change. | Emilio Jesus Gallego Arias | 2017-12-10 |
| | | | | | | |||
| | | * | | | [ci] Download ci-sf archives into the proper CI build dir. | Emilio Jesus Gallego Arias | 2017-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. | Théo Zimmermann | 2017-12-08 |
| | | | | | |||
* | | | | | Merge PR #6158: Allows a level in the raw and glob printers | Maxime Dénès | 2017-12-08 |
|\ \ \ \ \ | |||
| | * | | | | [ci] CoLoR has moved to github | Emilio Jesus Gallego Arias | 2017-12-07 |
| |/ / / / |/| | | | | | | | | | | | | | | Closes #6194 . | ||
| | | * | | Overlay for Equations. | Gaëtan Gilbert | 2017-12-06 |
| |_|/ / |/| | | | |||
* | | | | [ci] Test coqchk on the CompCert target. | Théo Zimmermann | 2017-11-30 |
| | | | | |||
* | | | | [ci] [vst] Shorten compilation time to avoid Travis timeouts. | Emilio Jesus Gallego Arias | 2017-11-28 |
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | 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. |