aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2017-11-20Merge PR #6183: [plugins] Prepare plugin API for functional handling of state.Maxime Dénès
2017-11-20Merge PR #6163: [dev] Remove deprecation warning from `base_include`Maxime Dénès
2017-11-19[plugins] Prepare plugin API for functional handling of state.Emilio Jesus Gallego Arias
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.
2017-11-16Merge PR #6148: [api] Another large deprecation, `Nameops` and friends.Maxime Dénès
2017-11-15[dev] Remove deprecation warning from `base_include`Emilio Jesus Gallego Arias
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.
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
2017-11-13Change OCAMLRUNPARAM warning to mention OCaml 4.06Paul Steckler
2017-11-13Merge PR #6098: [api] Move structures deprecated in the API to the core.Maxime Dénès
2017-11-13Merge PR #6126: Fix ci-bignums.sh "missing ]" error.Maxime Dénès
2017-11-13Merge PR #6124: Adding a debugging printer for ident maps whose codomain ↵Maxime Dénès
type is unknown
2017-11-13Merge PR #6071: [ci] Add Ltac2Maxime Dénès
2017-11-13Merge PR #6065: [api] Deprecate all legacy uses of Names in core.Maxime Dénès
2017-11-09Fix 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-08Adding a debugging printer for ident maps whose codomain type is unknown.Hugo Herbelin
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.
2017-11-08Merge PR #6100: [api] Remove 8.7 ML-deprecated functions.Maxime Dénès
2017-11-08Merge PR #6086: [ci] Switch VST back to upstream.Maxime Dénès
2017-11-07[api] Remove 8.7 ML-deprecated functions.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
We do up to `Term` which is the main bulk of the changes.
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
This will allow to merge back `Names` with `API.Names`
2017-11-06Merge PR #6049: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" ↵Maxime Dénès
rules
2017-11-06Merge PR #1139: Add a linter.Maxime Dénès
2017-11-04[ci] Add Ltac2Jason Gross
2017-11-03Merge PR #6047: A generic printer for ltac valuesMaxime Dénès
2017-11-03Merge PR #6036: [toplevel] Export the last document seen after `Drop`.Maxime Dénès
2017-11-03Merge PR #6031: [ci] Switch back to upstream version of Math-Classes and Corn.Maxime Dénès
2017-11-03Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in ↵Maxime Dénès
dev/doc/changes.
2017-11-03Merge PR #6024: Update of Coq version historyMaxime Dénès
2017-11-02Using a specific function to register vernac printers.Hugo Herbelin
2017-11-01provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rulesMatej Košík
Originally, it was not possible to define a new vernacular command in the following way: VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY [ "SomeCmd" ] -> [ Feedback.msg_notice ?loc (Pp.str "some message") ] END because "loc : Loc.t" was not bound. This commit fixes that, i.e. the location of the custom Vernacular command (within *.v file) is made available as "loc" variable bound on the right side of "->" .
2017-10-30[ci] Switch VST back to upstream.Théo Zimmermann
This finally closes #5994.
2017-10-28[toplevel] Export the last document seen after `Drop`.Emilio Jesus Gallego Arias
After `Drop`, `Coqtop.drop_last_doc` will contain the current document used by `Coqloop`. This is useful for people wanting to restart Coq after a `Drop`.
2017-10-27[ci] Switch back to upstream version of Math-Classes and Corn.Théo Zimmermann
2017-10-27Mention the migration from Bugzilla to GitHub issues in dev/doc/changes.Théo Zimmermann
2017-10-27Merge PR #6015: [general] Remove Econstr dependency from `intf`Maxime Dénès
2017-10-27Merge PR #677: Trunk+abstracting injection flagsMaxime Dénès
2017-10-26Passing around the flag for injection so that tactics calling inj atHugo Herbelin
ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug #5281.
2017-10-26Updating version history wrt 8.7.Hugo Herbelin
2017-10-26Updating version history wrt 8.6.Hugo Herbelin
2017-10-26Updating version history wrt 8.5.Hugo Herbelin
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
To this extent we factor out the relevant bits to a new file, ltac_pretype.
2017-10-25Linter: check that files end with newlines.Gaëtan Gilbert
We use git check-attr to look at the same files as git diff --check.
2017-10-25Put newlines at the end of files.Gaëtan Gilbert
2017-10-25Add linter.Gaëtan Gilbert
2017-10-25Merge PR #6003: Point HoTT back at master, which now supports Coq masterMaxime Dénès
2017-10-23Point HoTT back at master, which now supports Coq masterJason Gross
2017-10-20Switch testing branch back to CompCert upstream.Théo Zimmermann
This follows the merge of AbsInt/CompCert#191.
2017-10-20Merge PR #5984: CI: build lambdaRust (which depends on Iris) rather than ↵Maxime Dénès
just Iris
2017-10-19rename ci-iris-coq -> ci-iris-lambda-rustRalf Jung
2017-10-19CI: build lambdaRust (which depends on Iris) rather than just IrisRalf Jung
2017-10-18Bugzilla autolink: avoid linking inside links (fix #5974).Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-24 23:52:45 +0000