aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\
* | Revert "[ci] Temporal workaround for checker non-backwards compatible change."Gravatar Théo Zimmermann2017-12-12
| | | | | | | | This reverts commit 5d4cf69a3d7d472b54b5decc8400164b87e9a73f.
* | Merge PR #6331: Linter: skip PRs older than the linter.Gravatar Maxime Dénès2017-12-11
|\ \
* \ \ Merge PR #6368: [api] Remove yet another type alias.Gravatar Maxime Dénès2017-12-11
|\ \ \
* \ \ \ Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Gravatar Maxime Dénès2017-12-11
|\ \ \ \
* \ \ \ \ Merge PR #6358: [ci] Download ci-sf archives into the proper CI build dir.Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6351: Fix a copy-paste error in ci-ltac2.Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6346: [ci] CoLoR has moved to githubGravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \ \
| | | | | | | * [build] Remove coqmktop in favor of ocamlfind.Gravatar Emilio Jesus Gallego Arias2017-12-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | | | [ci] Temporal workaround for checker non-backwards compatible change.Gravatar Emilio Jesus Gallego Arias2017-12-10
| | | | | | | |
| | | | | * | | [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
| |_|_|_|/ / / |/| | | | | |
| | | | | | * [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
| |_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
| | | * | | [ci] Download ci-sf archives into the proper CI build dir.Gravatar Emilio Jesus Gallego Arias2017-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.Gravatar Théo Zimmermann2017-12-08
| | | | |
* | | | | Merge PR #6158: Allows a level in the raw and glob printersGravatar Maxime Dénès2017-12-08
|\ \ \ \ \
| | * | | | [ci] CoLoR has moved to githubGravatar Emilio Jesus Gallego Arias2017-12-07
| | | | | | | | | | | | | | | | | | | | | | | | Closes #6194 .
* | | | | | Merge PR #6267: Fix PR merge script.Gravatar Maxime Dénès2017-12-07
|\ \ \ \ \ \ | |_|/ / / / |/| | | | |
| | | | * | Overlay for Equations.Gravatar Gaëtan Gilbert2017-12-06
| |_|_|/ / |/| | | |
| | | | * Linter: skip PRs older than the linter.Gravatar Gaëtan Gilbert2017-12-06
| |_|_|/ |/| | |
* | | | uninstall doc dir, not dev (which is not installed), #6007Gravatar Paul Steckler2017-12-01
| | | |
* | | | Merge PR #736: [ci] Test coqchk on the CompCert target.Gravatar Maxime Dénès2017-12-01
|\ \ \ \
* \ \ \ \ Merge PR #6244: [lib] [api] Introduce record for `object_prefix`Gravatar Maxime Dénès2017-11-30
|\ \ \ \ \
| | * | | | [ci] Test coqchk on the CompCert target.Gravatar Théo Zimmermann2017-11-30
| |/ / / / |/| | | |
* | | | | Merge PR #6269: [ci] [vst] Shorten compilation time to avoid Travis timeouts.Gravatar Maxime Dénès2017-11-30
|\ \ \ \ \
| | | * | | Fix usage comment.Gravatar Théo Zimmermann2017-11-29
| | | | | |
| | | * | | This script apparently uses bash-specific features.Gravatar Théo Zimmermann2017-11-29
| | | | | |
| | | * | | Fix PR merge script.Gravatar Théo Zimmermann2017-11-29
| |_|/ / / |/| | | | | | | | | | | | | | Was still relying on the existence of user-configured /pr/.
| | * | | [lib] [api] Introduce record for `object_prefix`Gravatar Emilio Jesus Gallego Arias2017-11-29
| | | |/ | | |/| | | | | | | | | | | | | This is a minor cleanup adding a record in a try to structure the state living in `Lib`.
* | | | Add PR backport script.Gravatar Théo Zimmermann2017-11-28
| | | |
| * | | [ci] [vst] Shorten compilation time to avoid Travis timeouts.Gravatar Emilio Jesus Gallego Arias2017-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.
* | | Merge PR #6259: Add PR merge script.Gravatar Maxime Dénès2017-11-28
|\ \ \
| * | | Add PR merge script.Gravatar Maxime Dénès2017-11-28
| |/ /
* | | Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\ \ \
* \ \ \ Merge PR #6248: [api] Remove aliases of `Evar.t`Gravatar Maxime Dénès2017-11-28
|\ \ \ \ | |_|/ / |/| | |
| | | * Adding overlay for ltac2.Gravatar Hugo Herbelin2017-11-27
| | | |
* | | | Merge PR #6227: Linter: do not lint untracked files.Gravatar Maxime Dénès2017-11-27
|\ \ \ \ | |_|_|/ |/| | |
| | * | [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
| |/ / |/| | | | | | | | | | | There don't really bring anything, we also correct some minor nits with the printing function.
| | * Overlay for stronger restrict_universe_context.Gravatar Gaëtan Gilbert2017-11-25
| |/ |/|
* | Merge PR #876: In omega or romega, recognizing Z and nat modulo conversionGravatar Maxime Dénès2017-11-24
|\ \
* \ \ Merge PR #6197: [plugin] Remove LocalityFixme über hack.Gravatar Maxime Dénès2017-11-24
|\ \ \
* \ \ \ Merge PR #6186: [api] Miscellaneous consolidation.Gravatar Maxime Dénès2017-11-23
|\ \ \ \
| | | | * Linter: do not lint untracked files.Gravatar Gaëtan Gilbert2017-11-23
| |_|_|/ |/| | |
| | | * Adding ad hoc overlay for sf/vfa.Gravatar Hugo Herbelin2017-11-23
| |_|/ |/| |
* | | Merge PR #6189: Disable whitespace linter for .out files.Gravatar Maxime Dénès2017-11-23
|\ \ \
| | | * [plugin] Remove LocalityFixme über hack.Gravatar Emilio Jesus Gallego Arias2017-11-22
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
| |/ |/| | | | | | | | | 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.
* | [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
| | | | | | | | | | | | | | | | | | | | | | 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.
* | Merge PR #6185: [parser] Remove unnecessary statically initialized hook.Gravatar Maxime Dénès2017-11-21
|\ \
* \ \ Merge PR #6168: Add Equations to CIGravatar Maxime Dénès2017-11-21
|\ \ \
| | | * Disable whitespace linter for .out files.Gravatar Gaëtan Gilbert2017-11-20
| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 12:18:48 +0000