| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2017-11-27 | Adding overlay for ltac2. | Hugo Herbelin | |
| 2017-11-27 | Merge PR #6227: Linter: do not lint untracked files. | Maxime Dénès | |
| 2017-11-26 | [api] Remove aliases of `Evar.t` | Emilio Jesus Gallego Arias | |
| There don't really bring anything, we also correct some minor nits with the printing function. | |||
| 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-24 | Merge PR #6197: [plugin] Remove LocalityFixme über hack. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |