aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-12[warnings] Disable warning 59 [assignment to a non-mutable value] to make ↵Emilio Jesus Gallego Arias
flambda happy. See issue #8043. Using `[@@@ocaml.warning "-59"]` to disable this fails, it seems like an OCaml bug.
2018-07-12[ci] Remove warning jobs in favor of default `-warn-error yes`Emilio Jesus Gallego Arias
As discussed in #6930, we remove the warnings jobs and instead do require the developers to submit a clean build.
2018-07-12Merge PR #7871: [ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0Gaëtan Gilbert
2018-07-11[ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0Emilio Jesus Gallego Arias
- 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.
2018-07-11Merge PR #7998: [coqpp] Move to its own directory.Pierre-Marie Pédrot
2018-07-11Merge PR #8035: Fix #8033: Tactic assert-suceeds has a typo in its name in ↵Théo Zimmermann
the manual
2018-07-11Merge PR #8021: Get rid of horrendous hack limiting the size of parsed integersPierre-Marie Pédrot
2018-07-11Merge PR #8002: make-both-single-timing-files: fix --sort-by=diffJason Gross
2018-07-11Merge PR #7898: Remove camlp4 remainsEmilio Jesus Gallego Arias
2018-07-11[coqpp] Move to its own directory.Emilio Jesus Gallego Arias
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.
2018-07-11Merge PR #7984: Compile `coqpp` inside the `bin/` folder and make it ↵Emilio Jesus Gallego Arias
available after installation
2018-07-11Merge PR #8031: Remove auto-retry in GitLab CI now that @coqbot is handling it.Emilio Jesus Gallego Arias
2018-07-10Compile coqpp inside the bin/ folder and make it available after installation.Pierre-Marie Pédrot
2018-07-10Merge PR #8036: [travis] Remove even more jobs.Emilio Jesus Gallego Arias
2018-07-10Merge PR #8034: [travis] Try to workaround the repeated APT failures by ↵Emilio Jesus Gallego Arias
using Jason Gross's suggestion.
2018-07-10[travis] Remove even more jobs.Théo Zimmermann
Users who want to test external projects should be encouraged to activate GitLab CI as is documented in dev/ci/README.md.
2018-07-10fixed typo for assert_suceedcharguer
2018-07-10[travis] Try to workaround the repeated APT failures by using Jason Gross's ↵Théo Zimmermann
suggestion.
2018-07-10Remove auto-retry in GitLab CI now that @coqbot is handling it.Théo Zimmermann
2018-07-10Merge PR #7899: My recent improvements to the backport script.Maxime Dénès
2018-07-10Merge PR #7983: Turn a dead branch into an assertion failure in VM reification.Maxime Dénès
2018-07-10Merge PR #8028: Fix a few typosThéo Zimmermann
2018-07-10Merge PR #8025: Fix rst syntax for `quote ident {ident}`Théo Zimmermann
2018-07-10Add new options --no-conflict and --no-signature-check to backport script.Théo Zimmermann
2018-07-10Fix typo in doc/proof-engine/tactics.rst.whitequark
2018-07-10Fix typo in Init.Logic.whitequark
2018-07-09Merge PR #7920: Generic syntax for attributesMaxime Dénès
2018-07-09Fix rst syntax for `quote ident {ident}`Joachim Breitner
2018-07-09Merge PR #7884: Fix #5719: Uncaught exception Invalid_argument.Matthieu Sozeau
2018-07-08Merge PR #8015: Output UTF-8 explicitly in timing toolsJason Gross
2018-07-08Get rid of horrendous hack limiting the size of parsed integersMaxime Dénès
2018-07-08Merge PR #7985: Remove letouzey from CODEOWNERS since he left the Coq ↵Maxime Dénès
organization.
2018-07-08Merge PR #8020: Modify URLs in xml-protocol.mdThéo Zimmermann
2018-07-08Modify URLs in xml-protocol.mdRin Arakaki
2018-07-08Modify URLs in xml-protocol.mdRin Arakaki
2018-07-08Merge PR #7843: Remove Emacs modesMaxime Dénès
2018-07-08Mention the removal of Emacs modes in CHANGES.Théo Zimmermann
2018-07-08Remove Emacs modes.Théo Zimmermann
They are not used anymore. People should use Proof-General (and optionally Company-Coq) instead.
2018-07-07make diff sort by difference, not absolute differenceRalf Jung
2018-07-07make-both-single-timing-files: fix --sort-by=diffRalf Jung
2018-07-07Output UTF-8 explicitly in timing toolsJasper Hugunin
2018-07-07Merge PR #7921: Archive the `gallina` toolMaxime Dénès
2018-07-07Add an overlay.Pierre-Marie Pédrot
2018-07-07Merge PR #7956: Rebuild coqtop$(EXE) in "make coqbinaries" in addition to ↵Enrico Tassi
coqtop.opt$(EXE).
2018-07-07Introduce a Pcoq.Entry module for functions that ought to be exported.Pierre-Marie Pédrot
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.
2018-07-07Remove dead code that used to be there for CamlpX compatibility.Pierre-Marie Pédrot
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.
2018-07-07Merge PR #8005: Fix compilation of Coq with camlp5 master branch.Emilio Jesus Gallego Arias
2018-07-06Merge PR #8001: Cache the build of the Nix package using Cachix.Gaëtan Gilbert
2018-07-06Merge PR #7821: [refine] obey the use_unification_heuristics flagPierre-Marie Pédrot
2018-07-06Merge PR #8008: Add test for #8004.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:28:14 +0000