aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-16bin,oct,hex conversions positive,Z,N,nat<->stringJason Gross
2018-07-16Merge PR #8023: Introduce a team of code owners for the CI system.Maxime Dénès
2018-07-16Merge PR #8066: [ltac] Remove unused functions.Pierre-Marie Pédrot
2018-07-14[ltac] Remove unused functions / constructors.Emilio Jesus Gallego Arias
Catched by compiling the ml files from ml4.
2018-07-13Merge PR #8057: Fixed typos, wording and grammar errors in the Preamble of ↵Théo Zimmermann
the Reference Manual (Introduction, Credits).
2018-07-13Merge PR #6930: Make -warn-error fail on warnings emitted by coqc on stdlib.Emilio Jesus Gallego Arias
2018-07-13Make -warn-error fail on warnings emitted by coqc on stdlib.Maxime Dénès
We turn all Coq warnings that are on by default into errors.
2018-07-12Fixed typos, wording and grammar errors in the Preamble of the Reference ↵Zeimer
Manual (Introduction, Credits).
2018-07-12Merge PR #8041: [ci] Remove warning jobs in favor of default `-warn-error yes`Gaëtan Gilbert
2018-07-12Merge PR #7907: Tactic deprecation machineryPierre-Marie Pédrot
2018-07-12Merge PR #8051: Clean-up user-overlays folder.Emilio Jesus Gallego Arias
2018-07-12Clean-up user-overlays folder.Théo Zimmermann
2018-07-12[warnings] Disable warning 58 "no cmx file was found in path"Emilio Jesus Gallego Arias
See https://github.com/ocaml/num/issues/9
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-12Tactic deprecation machineryMaxime Dénès
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.".
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-09Introduce a team of code owners for the CI system.Théo Zimmermann
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.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:00:07 +0000