| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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 | |
| 2017-11-23 | Merge PR #6186: [api] Miscellaneous consolidation. | Maxime Dénès | |
| 2017-11-23 | Linter: do not lint untracked files. | Gaëtan Gilbert | |
| 2017-11-23 | Adding ad hoc overlay for sf/vfa. | Hugo Herbelin | |
| 2017-11-23 | Merge PR #6189: Disable whitespace linter for .out files. | Maxime Dénès | |
| 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-21 | [api] Miscellaneous consolidation + moves to engine. | Emilio Jesus Gallego Arias | |
| We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization. | |||
| 2017-11-21 | [printing] Deprecate all printing functions accessing the global proof. | Emilio Jesus Gallego Arias | |
| We'd like to handle proofs functionally we thus recommend not to use printing functions without an explicit context. We also adapt most of the code, making more explicit where the printing environment is coming from. An open task is to refactor some code so we gradually make the `Pfedit.get_current_context ()` disappear. | |||
| 2017-11-21 | Merge PR #6185: [parser] Remove unnecessary statically initialized hook. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |