aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* 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] 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
| |_|_|/ |/| | |
* | | | Merge PR #6047: A generic printer for ltac valuesGravatar Maxime Dénès2017-11-03
|\ \ \ \
* \ \ \ \ Merge PR #6036: [toplevel] Export the last document seen after `Drop`.Gravatar Maxime Dénès2017-11-03
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6031: [ci] Switch back to upstream version of Math-Classes and Corn.Gravatar Maxime Dénès2017-11-03
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in ↵Gravatar Maxime Dénès2017-11-03
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | dev/doc/changes.
* \ \ \ \ \ \ \ Merge PR #6024: Update of Coq version historyGravatar Maxime Dénès2017-11-03
|\ \ \ \ \ \ \ \
| | | | | * | | | Using a specific function to register vernac printers.Gravatar Hugo Herbelin2017-11-02
| |_|_|_|/ / / / |/| | | | | | |
| | | | | | * | provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rulesGravatar Matej Košík2017-11-01
| |_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 "->" .
| | | | | | * [ci] Switch VST back to upstream.Gravatar Théo Zimmermann2017-10-30
| | | | |_|/ | | | |/| | | | | | | | | | | | | | This finally closes #5994.
| | | | * | [toplevel] Export the last document seen after `Drop`.Gravatar Emilio Jesus Gallego Arias2017-10-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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`.
| | | * | | [ci] Switch back to upstream version of Math-Classes and Corn.Gravatar Théo Zimmermann2017-10-27
| | | |/ /
| | * / / Mention the migration from Bugzilla to GitHub issues in dev/doc/changes.Gravatar Théo Zimmermann2017-10-27
| | |/ /
* | | | Merge PR #6015: [general] Remove Econstr dependency from `intf`Gravatar Maxime Dénès2017-10-27
|\ \ \ \
* \ \ \ \ Merge PR #677: Trunk+abstracting injection flagsGravatar Maxime Dénès2017-10-27
|\ \ \ \ \ | |_|_|/ / |/| | | |
| * | | | Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-10-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | * | Updating version history wrt 8.7.Gravatar Hugo Herbelin2017-10-26
| | | | |
| | | * | Updating version history wrt 8.6.Gravatar Hugo Herbelin2017-10-26
| | | | |
| | | * | Updating version history wrt 8.5.Gravatar Hugo Herbelin2017-10-26
| |_|/ / |/| | |
| | * | [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
| |/ / | | | | | | | | | | | | To this extent we factor out the relevant bits to a new file, ltac_pretype.
| | * Linter: check that files end with newlines.Gravatar Gaëtan Gilbert2017-10-25
| | | | | | | | | | | | We use git check-attr to look at the same files as git diff --check.
| | * Put newlines at the end of files.Gravatar Gaëtan Gilbert2017-10-25
| | |
| | * Add linter.Gravatar Gaëtan Gilbert2017-10-25
| | |
* | | Merge PR #6003: Point HoTT back at master, which now supports Coq masterGravatar Maxime Dénès2017-10-25
|\ \ \
| * | | Point HoTT back at master, which now supports Coq masterGravatar Jason Gross2017-10-23
| | | |
* | | | Switch testing branch back to CompCert upstream.Gravatar Théo Zimmermann2017-10-20
| |/ / |/| | | | | | | | This follows the merge of AbsInt/CompCert#191.
* | | Merge PR #5984: CI: build lambdaRust (which depends on Iris) rather than ↵Gravatar Maxime Dénès2017-10-20
|\ \ \ | | | | | | | | | | | | just Iris
| * | | rename ci-iris-coq -> ci-iris-lambda-rustGravatar Ralf Jung2017-10-19
| | | |
| * | | CI: build lambdaRust (which depends on Iris) rather than just IrisGravatar Ralf Jung2017-10-19
| |/ /
* / / Bugzilla autolink: avoid linking inside links (fix #5974).Gravatar Gaëtan Gilbert2017-10-18
|/ /
* | Merge PR #540: [configure] Support for flambda flags.Gravatar Maxime Dénès2017-10-10
|\ \
* \ \ Merge PR #1067: Iris CI: use opam to install dependenciesGravatar Maxime Dénès2017-10-10
|\ \ \
| | * | [configure] Support for flambda flags.Gravatar Emilio Jesus Gallego Arias2017-10-10
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | We add a new option to configure `-flambda-opts` to allow passing custom flags to flambda. Example: ``` ./configure -flambda-opts "-O3 -unbox-closures" ```
* | | Merge PR #1115: Autolink to Github PRs from BugzillaGravatar Maxime Dénès2017-10-09
|\ \ \
* \ \ \ Merge PR #1117: [ci] Remove temporary bignums overlay.Gravatar Maxime Dénès2017-10-09
|\ \ \ \ | |_|_|/ |/| | |
* | | | Extract changes to the XML protocol from its docGravatar Théo Zimmermann2017-10-06
| | | |
* | | | Make the XML protocol doc more version-independentGravatar Théo Zimmermann2017-10-06
| | | |
* | | | Merge PR #1112: Fix GeoCoq CI and remove it from allowed failuresGravatar Maxime Dénès2017-10-05
|\ \ \ \
| | * | | [ci] Remove temporary bignums overlay.Gravatar Théo Zimmermann2017-10-04
| |/ / / |/| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 08:02:02 +0000