aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| | * | | Tactic deprecation machineryGravatar Maxime Dénès2018-07-12
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We make it possible to deprecate tactics defined by `Ltac`, `Tactic Notation` or ML. For the first two variants, we anticipate the syntax of attributes: `#[deprecated(since = "XX", note = "YY")]` In ML, the syntax is: ``` let reflexivity_depr = let open CWarnings in { since = "8.5"; note = "Use admit instead." } TACTIC EXTEND reflexivity DEPRECATED reflexivity_depr [ "reflexivity" ] -> [ Tactics.intros_reflexivity ] END ``` A warning is shown at the point where the tactic is used (either a direct call or when defining another tactic): Tactic `foo` is deprecated since XX. YY YY is typically meant to be "Use bar instead.".
| * | | [ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0Gravatar Emilio Jesus Gallego Arias2018-07-11
|/ / / | | | | | | | | | | | | | | | - We update the OCaml version used in the base CI image. - Windows / OSX image building is also updated to use newer OCaml. - We also update Dune to 1.0.0.
* | | Merge PR #7998: [coqpp] Move to its own directory.Gravatar Pierre-Marie Pédrot2018-07-11
|\ \ \
* \ \ \ Merge PR #8035: Fix #8033: Tactic assert-suceeds has a typo in its name in ↵Gravatar Théo Zimmermann2018-07-11
|\ \ \ \ | | | | | | | | | | | | | | | the manual
* \ \ \ \ Merge PR #8021: Get rid of horrendous hack limiting the size of parsed integersGravatar Pierre-Marie Pédrot2018-07-11
|\ \ \ \ \
* \ \ \ \ \ Merge PR #8002: make-both-single-timing-files: fix --sort-by=diffGravatar Jason Gross2018-07-11
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7898: Remove camlp4 remainsGravatar Emilio Jesus Gallego Arias2018-07-11
|\ \ \ \ \ \ \
| | | | | * | | [coqpp] Move to its own directory.Gravatar Emilio Jesus Gallego Arias2018-07-11
| |_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Coqpp has nothing to do with `grammar`, we thus place it in its own directory, which will prove convenient in more modular build systems. Note that we add `coqpp` to the list of global includes, we could have indeed added some extra rules, but IMHO not worth it as hopefully proper containment will be soon checked by Dune.
* | | | | | | Merge PR #7984: Compile `coqpp` inside the `bin/` folder and make it ↵Gravatar Emilio Jesus Gallego Arias2018-07-11
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | available after installation
* \ \ \ \ \ \ \ Merge PR #8031: Remove auto-retry in GitLab CI now that @coqbot is handling it.Gravatar Emilio Jesus Gallego Arias2018-07-11
|\ \ \ \ \ \ \ \
| | | | | | | | * Export a function to apply toplevel tactic values in Tacinterp.Gravatar Pierre-Marie Pédrot2018-07-10
| |_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a function that keeps beeing asked or reimplemented. It doesn't hurt adding it to the Ltac API.
| | * | | | | | Compile coqpp inside the bin/ folder and make it available after installation.Gravatar Pierre-Marie Pédrot2018-07-10
| |/ / / / / / |/| | | | | |
* | | | | | | Merge PR #8036: [travis] Remove even more jobs.Gravatar Emilio Jesus Gallego Arias2018-07-10
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #8034: [travis] Try to workaround the repeated APT failures by ↵Gravatar Emilio Jesus Gallego Arias2018-07-10
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | using Jason Gross's suggestion.
| | * | | | | | | [travis] Remove even more jobs.Gravatar Théo Zimmermann2018-07-10
| |/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Users who want to test external projects should be encouraged to activate GitLab CI as is documented in dev/ci/README.md.
| | | | | | * | fixed typo for assert_suceedGravatar charguer2018-07-10
| |_|_|_|_|/ / |/| | | | | |
| * | | | | | [travis] Try to workaround the repeated APT failures by using Jason Gross's ↵Gravatar Théo Zimmermann2018-07-10
|/ / / / / / | | | | | | | | | | | | | | | | | | suggestion.
| * / / / / Remove auto-retry in GitLab CI now that @coqbot is handling it.Gravatar Théo Zimmermann2018-07-10
|/ / / / /
* | | | | Merge PR #7899: My recent improvements to the backport script.Gravatar Maxime Dénès2018-07-10
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7983: Turn a dead branch into an assertion failure in VM reification.Gravatar Maxime Dénès2018-07-10
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #8028: Fix a few typosGravatar Théo Zimmermann2018-07-10
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #8025: Fix rst syntax for `quote ident {ident}`Gravatar Théo Zimmermann2018-07-10
|\ \ \ \ \ \ \ \
| | | | * | | | | Add new options --no-conflict and --no-signature-check to backport script.Gravatar Théo Zimmermann2018-07-10
| |_|_|/ / / / / |/| | | | | | |
| | * | | | | | Fix typo in doc/proof-engine/tactics.rst.Gravatar whitequark2018-07-10
| | | | | | | |
| | * | | | | | Fix typo in Init.Logic.Gravatar whitequark2018-07-10
| |/ / / / / / |/| | | | | |
* | | | | | | Merge PR #7920: Generic syntax for attributesGravatar Maxime Dénès2018-07-09
|\ \ \ \ \ \ \
| | * | | | | | Fix rst syntax for `quote ident {ident}`Gravatar Joachim Breitner2018-07-09
| |/ / / / / / |/| | | | | |
* | | | | | | Merge PR #7884: Fix #5719: Uncaught exception Invalid_argument.Gravatar Matthieu Sozeau2018-07-09
|\ \ \ \ \ \ \
| | | | | | | * Introduce a team of code owners for the CI system.Gravatar Théo Zimmermann2018-07-09
| |_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This means that all the members of the team will receive a review request for PRs on the CI, but only one of them will need to approve the PR, and this will remove the review request for the others. Currently the team contains Emilio and Gaetan, the two former code owners of these files. It makes sense to start experimenting on this component since they had already decided to make their role symmetric. Updating the list of maintainers can be done by updating the list members, and without changing the CODEOWNER file.
* | | | | | | Merge PR #8015: Output UTF-8 explicitly in timing toolsGravatar Jason Gross2018-07-08
|\ \ \ \ \ \ \
| | | | | | | * Get rid of horrendous hack limiting the size of parsed integersGravatar Maxime Dénès2018-07-08
| |_|_|_|_|_|/ |/| | | | | |
* | | | | | | Merge PR #7985: Remove letouzey from CODEOWNERS since he left the Coq ↵Gravatar Maxime Dénès2018-07-08
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | organization.
* \ \ \ \ \ \ \ Merge PR #8020: Modify URLs in xml-protocol.mdGravatar Théo Zimmermann2018-07-08
|\ \ \ \ \ \ \ \
| * | | | | | | | Modify URLs in xml-protocol.mdGravatar Rin Arakaki2018-07-08
| | | | | | | | |
| * | | | | | | | Modify URLs in xml-protocol.mdGravatar Rin Arakaki2018-07-08
|/ / / / / / / /
* | | | | | | | Merge PR #7843: Remove Emacs modesGravatar Maxime Dénès2018-07-08
|\ \ \ \ \ \ \ \
| * | | | | | | | Mention the removal of Emacs modes in CHANGES.Gravatar Théo Zimmermann2018-07-08
| | | | | | | | |
| * | | | | | | | Remove Emacs modes.Gravatar Théo Zimmermann2018-07-08
|/ / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | They are not used anymore. People should use Proof-General (and optionally Company-Coq) instead.
| | | | | | | * make diff sort by difference, not absolute differenceGravatar Ralf Jung2018-07-07
| | | | | | | |
| | | | | | | * make-both-single-timing-files: fix --sort-by=diffGravatar Ralf Jung2018-07-07
| |_|_|_|_|_|/ |/| | | | | |
| | * | | | | Output UTF-8 explicitly in timing toolsGravatar Jasper Hugunin2018-07-07
| | | | | | |
* | | | | | | Merge PR #7921: Archive the `gallina` toolGravatar Maxime Dénès2018-07-07
|\ \ \ \ \ \ \
| | | | | | | * Add an overlay.Gravatar Pierre-Marie Pédrot2018-07-07
| | | | | | | |
* | | | | | | | Merge PR #7956: Rebuild coqtop$(EXE) in "make coqbinaries" in addition to ↵Gravatar Enrico Tassi2018-07-07
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | coqtop.opt$(EXE).
| | | | | | | | * Introduce a Pcoq.Entry module for functions that ought to be exported.Gravatar Pierre-Marie Pédrot2018-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.Gravatar Pierre-Marie Pédrot2018-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.Gravatar Emilio Jesus Gallego Arias2018-07-07
|\ \ \ \ \ \ \ \ | |_|_|_|/ / / / |/| | | | | | |
* | | | | | | | Merge PR #8001: Cache the build of the Nix package using Cachix.Gravatar Gaëtan Gilbert2018-07-06
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #7821: [refine] obey the use_unification_heuristics flagGravatar Pierre-Marie Pédrot2018-07-06
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #8008: Add test for #8004.Gravatar Théo Zimmermann2018-07-06
|\ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-30 00:36:46 +0000