Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #7898: Remove camlp4 remains | Emilio Jesus Gallego Arias | 2018-07-11 |
|\ | |||
* \ | Merge PR #7984: Compile `coqpp` inside the `bin/` folder and make it ↵ | Emilio Jesus Gallego Arias | 2018-07-11 |
|\ \ | | | | | | | | | | available after installation | ||
* \ \ | Merge PR #8031: Remove auto-retry in GitLab CI now that @coqbot is handling it. | Emilio Jesus Gallego Arias | 2018-07-11 |
|\ \ \ | |||
| | * | | Compile coqpp inside the bin/ folder and make it available after installation. | Pierre-Marie Pédrot | 2018-07-10 |
| |/ / |/| | | |||
* | | | Merge PR #8036: [travis] Remove even more jobs. | Emilio Jesus Gallego Arias | 2018-07-10 |
|\ \ \ | |||
* \ \ \ | Merge PR #8034: [travis] Try to workaround the repeated APT failures by ↵ | Emilio Jesus Gallego Arias | 2018-07-10 |
|\ \ \ \ | | | | | | | | | | | | | | | | using Jason Gross's suggestion. | ||
| | * | | | [travis] Remove even more jobs. | Théo Zimmermann | 2018-07-10 |
| |/ / / |/| | | | | | | | | | | | | | | | Users who want to test external projects should be encouraged to activate GitLab CI as is documented in dev/ci/README.md. | ||
| * | | | [travis] Try to workaround the repeated APT failures by using Jason Gross's ↵ | Théo Zimmermann | 2018-07-10 |
|/ / / | | | | | | | | | | suggestion. | ||
| * / | Remove auto-retry in GitLab CI now that @coqbot is handling it. | Théo Zimmermann | 2018-07-10 |
|/ / | |||
* | | Merge PR #7899: My recent improvements to the backport script. | Maxime Dénès | 2018-07-10 |
|\ \ | |||
* \ \ | Merge PR #7983: Turn a dead branch into an assertion failure in VM reification. | Maxime Dénès | 2018-07-10 |
|\ \ \ | |||
* \ \ \ | Merge PR #8028: Fix a few typos | Théo Zimmermann | 2018-07-10 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #8025: Fix rst syntax for `quote ident {ident}` | Théo Zimmermann | 2018-07-10 |
|\ \ \ \ \ | |||
| | | | * | | Add new options --no-conflict and --no-signature-check to backport script. | Théo Zimmermann | 2018-07-10 |
| |_|_|/ / |/| | | | | |||
| | * | | | Fix typo in doc/proof-engine/tactics.rst. | whitequark | 2018-07-10 |
| | | | | | |||
| | * | | | Fix typo in Init.Logic. | whitequark | 2018-07-10 |
| |/ / / |/| | | | |||
* | | | | Merge PR #7920: Generic syntax for attributes | Maxime Dénès | 2018-07-09 |
|\ \ \ \ | |||
| | * | | | Fix rst syntax for `quote ident {ident}` | Joachim Breitner | 2018-07-09 |
| |/ / / |/| | | | |||
* | | | | Merge PR #7884: Fix #5719: Uncaught exception Invalid_argument. | Matthieu Sozeau | 2018-07-09 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #8015: Output UTF-8 explicitly in timing tools | Jason Gross | 2018-07-08 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #7985: Remove letouzey from CODEOWNERS since he left the Coq ↵ | Maxime Dénès | 2018-07-08 |
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | organization. | ||
* \ \ \ \ \ \ | Merge PR #8020: Modify URLs in xml-protocol.md | Théo Zimmermann | 2018-07-08 |
|\ \ \ \ \ \ \ | |||
| * | | | | | | | Modify URLs in xml-protocol.md | Rin Arakaki | 2018-07-08 |
| | | | | | | | | |||
| * | | | | | | | Modify URLs in xml-protocol.md | Rin Arakaki | 2018-07-08 |
|/ / / / / / / | |||
* | | | | | | | Merge PR #7843: Remove Emacs modes | Maxime Dénès | 2018-07-08 |
|\ \ \ \ \ \ \ | |||
| * | | | | | | | Mention the removal of Emacs modes in CHANGES. | Théo Zimmermann | 2018-07-08 |
| | | | | | | | | |||
| * | | | | | | | Remove Emacs modes. | Théo Zimmermann | 2018-07-08 |
|/ / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | They are not used anymore. People should use Proof-General (and optionally Company-Coq) instead. | ||
| | * | | | | | Output UTF-8 explicitly in timing tools | Jasper Hugunin | 2018-07-07 |
| | | | | | | | |||
* | | | | | | | Merge PR #7921: Archive the `gallina` tool | Maxime Dénès | 2018-07-07 |
|\ \ \ \ \ \ \ | |||
| | | | | | | * | Add an overlay. | Pierre-Marie Pédrot | 2018-07-07 |
| | | | | | | | | |||
* | | | | | | | | Merge PR #7956: Rebuild coqtop$(EXE) in "make coqbinaries" in addition to ↵ | Enrico Tassi | 2018-07-07 |
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | coqtop.opt$(EXE). | ||
| | | | | | | | * | Introduce a Pcoq.Entry module for functions that ought to be exported. | Pierre-Marie Pédrot | 2018-07-07 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We deprecate the corresponding functions in Pcoq.Gram. The motivation is that the Gram module is used as an argument to Camlp5 functors, so that it is not stable by extension. Enforcing that its type is literally the one Camlp5 expects ensures robustness to extension statically. Some really internal functions have been bluntly removed. It is unlikely that they are used by external plugins. | ||
| | | | | | | | * | Remove dead code that used to be there for CamlpX compatibility. | Pierre-Marie Pédrot | 2018-07-07 |
| |_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Part of this code has been introduced very recently in 7c62654 in spite of the existence of a proper API. This means that this should be better documented. | ||
* | | | | | | | | Merge PR #8005: Fix compilation of Coq with camlp5 master branch. | Emilio Jesus Gallego Arias | 2018-07-07 |
|\ \ \ \ \ \ \ \ | |_|_|_|/ / / / |/| | | | | | | | |||
* | | | | | | | | Merge PR #8001: Cache the build of the Nix package using Cachix. | Gaëtan Gilbert | 2018-07-06 |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #7821: [refine] obey the use_unification_heuristics flag | Pierre-Marie Pédrot | 2018-07-06 |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #8008: Add test for #8004. | Théo Zimmermann | 2018-07-06 |
|\ \ \ \ \ \ \ \ \ \ | |||
| | | * | | | | | | | | [pkg:nix] Add more comments and allow overriding extra substituters. | Théo Zimmermann | 2018-07-06 |
| | | | | | | | | | | | |||
| * | | | | | | | | | | Add test for #8004. | Gaëtan Gilbert | 2018-07-06 |
|/ / / / / / / / / / | |||
| | | * / / / / / / | Fix compilation of Coq with camlp5 master branch. | Pierre-Marie Pédrot | 2018-07-06 |
| |_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There was a conflict in the name of an exported function. A good argument in favour of PR #7898. | ||
* | | | | | | | | | Merge PR #7990: Convert timing tool to python3 | Jason Gross | 2018-07-05 |
|\ \ \ \ \ \ \ \ \ | |||
| | * | | | | | | | | refine: obey the use_unification_heuristics flag | Matthieu Sozeau | 2018-07-05 |
| |/ / / / / / / / |/| | | | | | | | | |||
* | | | | | | | | | Merge PR #7991: Make Travis faster by removing more builds. | Emilio Jesus Gallego Arias | 2018-07-05 |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #7994: Make bin/ in makefile, not configure. | Emilio Jesus Gallego Arias | 2018-07-05 |
|\ \ \ \ \ \ \ \ \ \ | |||
| | | | * | | | | | | | [pkg:nix] Stop using lib.inNixShell. | Théo Zimmermann | 2018-07-05 |
| | | | | | | | | | | | |||
| | | | * | | | | | | | [pkg:nix] Change the download method. | Théo Zimmermann | 2018-07-05 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This will allow for better reuse of the cache when the URL is different but the archive is the same. | ||
| | | | * | | | | | | | [pkg:nix] Pass through the ocamlPackages version used to build. | Théo Zimmermann | 2018-07-05 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This will be useful for users wanting to build a plugin using this package. | ||
| | | | * | | | | | | | [pkg:nix] Cache the build using Cachix when signing key is set. | Théo Zimmermann | 2018-07-05 |
| |_|_|/ / / / / / / |/| | | | | | | | | | |||
| | * | | | | | | | | Remove some Travis jobs to make the build faster. | Théo Zimmermann | 2018-07-05 |
| |/ / / / / / / / |/| | | | | | | | | |||
| | | | | | | | * | Turn a dead branch into an assertion failure in VM reification. | Pierre-Marie Pédrot | 2018-07-05 |
| |_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In #7607, dead code that used to handle non-dependent return predicates was removed. This made the reification branch expecting non-functions in predicates dead code. We fix this by using an assert instead. |