| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-01-23 | Merge PR #6568: Cleanup scripts | Maxime Dénès | |
| 2018-01-16 | Source basic overlay before user overlays. | Gaëtan Gilbert | |
| 2018-01-16 | Cleanup shell expansions and quoting. | Gaëtan Gilbert | |
| 2018-01-12 | Merge PR #6483: Strong invariants in polymorphic definitions | Maxime Dénès | |
| 2018-01-11 | 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-06 | First stab at documenting the test suite. | Jasper Hugunin | |
| 2018-01-04 | Normalize Windows installer names. | Théo Zimmermann | |
| 2017-12-29 | 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-27 | 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-26 | Fix overlay selection for Circle CI. | Gaëtan Gilbert | |
| 2017-12-26 | Delete old overlays (leaving example) | Gaëtan Gilbert | |
| 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-19 | Merge PR #6400: Circle CI | 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 #6413: [econstr] Switch constrintern API to non-imperative style. | Maxime Dénès | |
| 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-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 | 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-10 | [ci] Temporal workaround for checker non-backwards compatible change. | Emilio Jesus Gallego Arias | |
| 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-06 | Overlay for Equations. | Gaëtan Gilbert | |
| 2017-11-30 | [ci] Test coqchk on the CompCert target. | 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-27 | Adding overlay for ltac2. | Hugo Herbelin | |
| 2017-11-25 | Overlay for stronger restrict_universe_context. | Gaëtan Gilbert | |
| 2017-11-24 | Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion | Maxime Dénès | |
| 2017-11-23 | Adding ad hoc overlay for sf/vfa. | Hugo Herbelin | |
| 2017-11-22 | [plugin] Remove LocalityFixme über hack. | Emilio Jesus Gallego Arias | |
| To that extent we introduce a new prototype vernacular extension macro `VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the proper parameters and attributes. This of course needs more refinement, in particular we should move `vernac_command` to its own file and make `Vernacentries` consistent wrt it. | |||
| 2017-11-20 | Add Equations to CI | Matthieu Sozeau | |
| 2017-11-13 | Merge PR #6126: Fix ci-bignums.sh "missing ]" error. | Maxime Dénès | |
| 2017-11-13 | Merge PR #6071: [ci] Add Ltac2 | Maxime Dénès | |
| 2017-11-09 | Fix ci-bignums.sh "missing ]" error. | Gaëtan Gilbert | |
| It made the test always fail so ci-common was always sourced. It's not quite idempotent as it adds COQBIN to PATH but it didn't lead to CI failure. | |||
| 2017-11-04 | [ci] Add Ltac2 | Jason Gross | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |