| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-17 | Add overlay for Coq-Equations for QuestionMark. | Siddharth Bhat | |
| The changed QuestionMark structure breaks Coq-Equations. Add an overlay to fix this. | |||
| 2018-07-17 | Change QuestionMark for better record field missing error message. | Siddharth Bhat | |
| While we were adding a new field into `QuestionMark`, we decided to go ahead and refactor the constructor to hold an actual record. This record now holds the name, obligations, and whether the evar represents a missing record field. This is used to provide better error messages on missing record fields. | |||
| 2018-07-16 | Merge PR #8069: Only check overlay extensions on git-tracked files | Gaëtan Gilbert | |
| 2018-07-16 | Only check overlay extensions on git-tracked files | Jason Gross | |
| This way, when editors leave over temporary files from editing user-overlays, we don't prevent commits unless they are added to git. | |||
| 2018-07-16 | Merge PR #8023: Introduce a team of code owners for the CI system. | Maxime Dénès | |
| 2018-07-16 | Merge 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-13 | Merge PR #8057: Fixed typos, wording and grammar errors in the Preamble of ↵ | Théo Zimmermann | |
| the Reference Manual (Introduction, Credits). | |||
| 2018-07-13 | Merge PR #6930: Make -warn-error fail on warnings emitted by coqc on stdlib. | Emilio Jesus Gallego Arias | |
| 2018-07-13 | Make -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-12 | Fixed typos, wording and grammar errors in the Preamble of the Reference ↵ | Zeimer | |
| Manual (Introduction, Credits). | |||
| 2018-07-12 | Merge PR #8041: [ci] Remove warning jobs in favor of default `-warn-error yes` | Gaëtan Gilbert | |
| 2018-07-12 | Merge PR #7907: Tactic deprecation machinery | Pierre-Marie Pédrot | |
| 2018-07-12 | Merge PR #8051: Clean-up user-overlays folder. | Emilio Jesus Gallego Arias | |
| 2018-07-12 | Clean-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-12 | Merge PR #7871: [ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0 | Gaëtan Gilbert | |
| 2018-07-12 | Tactic deprecation machinery | Maxime 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.0 | Emilio 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-11 | Merge PR #7998: [coqpp] Move to its own directory. | Pierre-Marie Pédrot | |
| 2018-07-11 | Merge PR #8035: Fix #8033: Tactic assert-suceeds has a typo in its name in ↵ | Théo Zimmermann | |
| the manual | |||
| 2018-07-11 | Merge PR #8021: Get rid of horrendous hack limiting the size of parsed integers | Pierre-Marie Pédrot | |
| 2018-07-11 | Merge PR #8002: make-both-single-timing-files: fix --sort-by=diff | Jason Gross | |
| 2018-07-11 | Merge PR #7898: Remove camlp4 remains | Emilio 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-11 | Merge PR #7984: Compile `coqpp` inside the `bin/` folder and make it ↵ | Emilio Jesus Gallego Arias | |
| available after installation | |||
| 2018-07-11 | Merge PR #8031: Remove auto-retry in GitLab CI now that @coqbot is handling it. | Emilio Jesus Gallego Arias | |
| 2018-07-10 | 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 | |
| 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-10 | fixed typo for assert_suceed | charguer | |
| 2018-07-10 | [travis] Try to workaround the repeated APT failures by using Jason Gross's ↵ | Théo Zimmermann | |
| suggestion. | |||
| 2018-07-10 | 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-09 | 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 | Introduce 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-08 | Merge PR #8015: Output UTF-8 explicitly in timing tools | Jason Gross | |
| 2018-07-08 | Get rid of horrendous hack limiting the size of parsed integers | Maxime Dénès | |
| 2018-07-08 | Merge PR #7985: Remove letouzey from CODEOWNERS since he left the Coq ↵ | Maxime Dénès | |
| organization. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |