| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-04 | [ci] Add Ltac2 | Jason Gross | |
| 2017-11-03 | Merge PR #6047: A generic printer for ltac values | Maxime Dénès | |
| 2017-11-03 | Merge PR #6036: [toplevel] Export the last document seen after `Drop`. | Maxime Dénès | |
| 2017-11-03 | Merge PR #6031: [ci] Switch back to upstream version of Math-Classes and Corn. | Maxime Dénès | |
| 2017-11-03 | Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in ↵ | Maxime Dénès | |
| dev/doc/changes. | |||
| 2017-11-03 | Merge PR #6024: Update of Coq version history | Maxime Dénès | |
| 2017-11-02 | Using a specific function to register vernac printers. | Hugo Herbelin | |
| 2017-11-01 | provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules | Matej 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-27 | Mention the migration from Bugzilla to GitHub issues in dev/doc/changes. | Théo Zimmermann | |
| 2017-10-27 | Merge PR #6015: [general] Remove Econstr dependency from `intf` | Maxime Dénès | |
| 2017-10-27 | Merge PR #677: Trunk+abstracting injection flags | Maxime Dénès | |
| 2017-10-26 | Passing around the flag for injection so that tactics calling inj at | Hugo 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-26 | Updating version history wrt 8.7. | Hugo Herbelin | |
| 2017-10-26 | Updating version history wrt 8.6. | Hugo Herbelin | |
| 2017-10-26 | Updating 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-25 | Linter: 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-25 | Put newlines at the end of files. | Gaëtan Gilbert | |
| 2017-10-25 | Add linter. | Gaëtan Gilbert | |
| 2017-10-25 | Merge PR #6003: Point HoTT back at master, which now supports Coq master | Maxime Dénès | |
| 2017-10-23 | Point HoTT back at master, which now supports Coq master | Jason Gross | |
| 2017-10-20 | Switch testing branch back to CompCert upstream. | Théo Zimmermann | |
| This follows the merge of AbsInt/CompCert#191. | |||
| 2017-10-20 | Merge PR #5984: CI: build lambdaRust (which depends on Iris) rather than ↵ | Maxime Dénès | |
| just Iris | |||
| 2017-10-19 | rename ci-iris-coq -> ci-iris-lambda-rust | Ralf Jung | |
| 2017-10-19 | CI: build lambdaRust (which depends on Iris) rather than just Iris | Ralf Jung | |
| 2017-10-18 | Bugzilla autolink: avoid linking inside links (fix #5974). | Gaëtan Gilbert | |
| 2017-10-10 | Merge PR #540: [configure] Support for flambda flags. | Maxime Dénès | |
| 2017-10-10 | Merge PR #1067: Iris CI: use opam to install dependencies | Maxime Dénès | |
| 2017-10-10 | [configure] Support for flambda flags. | Emilio Jesus Gallego Arias | |
| We add a new option to configure `-flambda-opts` to allow passing custom flags to flambda. Example: ``` ./configure -flambda-opts "-O3 -unbox-closures" ``` | |||
| 2017-10-09 | Merge PR #1115: Autolink to Github PRs from Bugzilla | Maxime Dénès | |
| 2017-10-09 | Merge PR #1117: [ci] Remove temporary bignums overlay. | Maxime Dénès | |
| 2017-10-06 | Extract changes to the XML protocol from its doc | Théo Zimmermann | |
| 2017-10-06 | Make the XML protocol doc more version-independent | Théo Zimmermann | |
| 2017-10-05 | Merge PR #1112: Fix GeoCoq CI and remove it from allowed failures | Maxime Dénès | |
| 2017-10-04 | [ci] Remove temporary bignums overlay. | Théo Zimmermann | |
| 2017-10-03 | autolink to Github PRs from Bugzilla | Paul Steckler | |
| 2017-10-03 | Merge PR #1104: Browser userscript to turn BZ#XXXX occurences into links. | Maxime Dénès | |
| 2017-10-03 | Fix GeoCoq build by using a shared CI configure. | Théo Zimmermann | |
| See also GeoCoq/GeoCoq#7. | |||
| 2017-10-03 | Merge PR #1023: dev/build/windows/makecoq_mingw.sh: install camlp5's META file | Maxime Dénès | |
| 2017-09-29 | start counting at 0... | Ralf Jung | |
| 2017-09-29 | Iris CI: use opam to determine std++ git commit | Ralf Jung | |
| 2017-09-27 | Browser userscript to turn BZ#XXXX occurences into links. | Gaëtan Gilbert | |
| 2017-09-22 | Merge PR #1055: Remove STM vernaculars | Maxime Dénès | |
| 2017-09-22 | Merge PR #1065: In gitlab set TRAVIS_BRANCH so user overlays will work as ↵ | Maxime Dénès | |
| expected. | |||
| 2017-09-21 | Do not reinstall preinstalled packages under AppVeyor. | Maxime Dénès | |
| It seems that reinstalling gcc can leave Cygwin in a strange state, where invocations of gcc fail suddenly. I haven't figure out exactly why, but this seems to fix it. | |||
| 2017-09-21 | Print Cygwin setup output rather than logging in to a file. | Maxime Dénès | |
| 2017-09-20 | In gitlab set TRAVIS_BRANCH so user overlays will work as expected. | Gaëtan Gilbert | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |