aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* 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
|\ \
| | * [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
|\ \ \ | |_|/ |/| |
* | | 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
| | | |
* | | | Merge PR #6183: [plugins] Prepare plugin API for functional handling of state.Gravatar Maxime Dénès2017-11-20
|\ \ \ \
* \ \ \ \ Merge PR #6163: [dev] Remove deprecation warning from `base_include`Gravatar Maxime Dénès2017-11-20
|\ \ \ \ \ | |_|_|_|/ |/| | | |
| | | * | Add Equations to CIGravatar Matthieu Sozeau2017-11-20
| |_|/ / |/| | |
| | | * [parser] Remove unnecessary statically initialized hook.Gravatar Emilio Jesus Gallego Arias2017-11-19
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to put any pattern in binders, prefixed by a quote."] its current placement as well as the hook don't make a lot of sense. In particular, they prevent parts of Coq working without linking the parser. To this purpose, we need to consolidate the `Constrexpr` utilities. While we are at it we do so and remove the `Topconstr` module which is fully redundant with `Constrexpr_ops`.
| | * [plugins] Prepare plugin API for functional handling of state.Gravatar Emilio Jesus Gallego Arias2017-11-19
| |/ |/| | | | | | | | | | | | | To this purpose we allow plugins to register functions that will modify the state. This is not used yet, but will be used soon when we remove the global handling of the proof state.
* | Merge PR #6148: [api] Another large deprecation, `Nameops` and friends.Gravatar Maxime Dénès2017-11-16
|\ \
| | * [dev] Remove deprecation warning from `base_include`Gravatar Emilio Jesus Gallego Arias2017-11-15
| |/ |/| | | | | | | | | | | | | | | The warning created problems as OCaml restored the color printing tags when printing it, so users doing `Drop` and then `go ()` got color printing back after the warning. We should guard the console on `Drop` better, but this requires some (much needed) refactoring work in the toplevel.
| * [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
| |
* | Change OCAMLRUNPARAM warning to mention OCaml 4.06Gravatar Paul Steckler2017-11-13
|/
* Merge PR #6098: [api] Move structures deprecated in the API to the core.Gravatar Maxime Dénès2017-11-13
|\
* \ Merge PR #6126: Fix ci-bignums.sh "missing ]" error.Gravatar Maxime Dénès2017-11-13
|\ \
* \ \ Merge PR #6124: Adding a debugging printer for ident maps whose codomain ↵Gravatar Maxime Dénès2017-11-13
|\ \ \ | | | | | | | | | | | | type is unknown
* \ \ \ Merge PR #6071: [ci] Add Ltac2Gravatar Maxime Dénès2017-11-13
|\ \ \ \
* \ \ \ \ Merge PR #6065: [api] Deprecate all legacy uses of Names in core.Gravatar Maxime Dénès2017-11-13
|\ \ \ \ \
| | | | * | Fix ci-bignums.sh "missing ]" error.Gravatar Gaëtan Gilbert2017-11-09
| |_|_|/ / |/| | | | | | | | | | | | | | | | | | | 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.
| | | * | Adding a debugging printer for ident maps whose codomain type is unknown.Gravatar Hugo Herbelin2017-11-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Actually, ocaml is apparently doing well. If there is a printer for 'a Id.Map.t and another for say Id.t Id.Map.id, it uses the most defined existing ones, so, it is apparently not a problem to have overlapping printer.
* | | | | Merge PR #6100: [api] Remove 8.7 ML-deprecated functions.Gravatar Maxime Dénès2017-11-08
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6086: [ci] Switch VST back to upstream.Gravatar Maxime Dénès2017-11-08
|\ \ \ \ \ \ | |_|_|_|/ / |/| | | | |
| | * | | | [api] Remove 8.7 ML-deprecated functions.Gravatar Emilio Jesus Gallego Arias2017-11-07
| |/ / / / |/| | | |
| | | | * [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | |/ | | |/| | | | | | | | | We do up to `Term` which is the main bulk of the changes.
| | * | [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| |/ / |/| | | | | | | | This will allow to merge back `Names` with `API.Names`
* | | Merge PR #6049: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" ↵Gravatar Maxime Dénès2017-11-06
|\ \ \ | | | | | | | | | | | | rules
* \ \ \ Merge PR #1139: Add a linter.Gravatar Maxime Dénès2017-11-06
|\ \ \ \
| | | | * [ci] Add Ltac2Gravatar Jason Gross2017-11-04
| |_|_|/ |/| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 17:05:11 +0000