Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Remove declare_object for SsrHave NoTCResolution. | Maxime Dénès | 2018-07-19 |
| | | | | | | | IIUC, this was a hack to make `Set SsrHave NoTCResolution` behave like `Global Set SsrHave NoTCResolution`. I don't think it is needed (just let the user write the desired locality), but if it is, the right way of doing it is to let clients of Goptions specify a default locality. | ||
* | Merge PR #8054: [dev] Autogenerate OCaml dev files. | Enrico Tassi | 2018-07-18 |
|\ | |||
* \ | Merge PR #7897: Remove fourier plugin | Enrico Tassi | 2018-07-18 |
|\ \ | |||
* \ \ | Merge PR #8068: [build] Build Coq and plugins with `-strict-sequence` | Enrico Tassi | 2018-07-18 |
|\ \ \ | |||
* \ \ \ | Merge PR #8060: Remove useless libobject in proof_using | Enrico Tassi | 2018-07-18 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #8055: Fast accumulator check in native compilation | Maxime Dénès | 2018-07-17 |
|\ \ \ \ \ | |||
| | | | * | | Remove fourier plugin | Maxime Dénès | 2018-07-17 |
| |_|_|/ / |/| | | | | | | | | | | | | | | As stated in the manual, the fourier tactic is subsumed by lra. | ||
* | | | | | 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 | 2018-07-16 |
|/ / / / / | | | | | | | | | | | | | | | | | | | | | This way, when editors leave over temporary files from editing user-overlays, we don't prevent commits unless they are added to git. | ||
* | | | | | 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-16 |
|\ \ \ \ \ \ | |||
| | | | | * | | [build] Build Coq and plugins with `-strict-sequence` | Emilio Jesus Gallego Arias | 2018-07-14 |
| |_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | Fixes #8067. This is becoming the default in many developments, so it makes sense to require it too, both for Coq and for Plugins. | ||
| * | | | | | [ltac] Remove unused functions / constructors. | Emilio Jesus Gallego Arias | 2018-07-14 |
|/ / / / / | | | | | | | | | | | | | | | | Catched by compiling the ml files from ml4. | ||
* | | | | | Merge PR #8057: Fixed typos, wording and grammar errors in the Preamble of ↵ | Théo Zimmermann | 2018-07-13 |
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | | the Reference Manual (Introduction, Credits). | ||
| | | | * | | Remove useless libobject in proof_using | Maxime Dénès | 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 | 2018-07-13 |
|/ / / / / / | | | | | | | | | | | | | | | | | | | We turn all Coq warnings that are on by default into errors. | ||
| | | * | | | Generate type-specific code for is_accu in native compilation of fixpoints. | Pierre-Marie Pédrot | 2018-07-13 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is much more efficient than using Nativevalues.is_accu function which incurs a lot of irrelevant checks on its argument. | ||
| | | * | | | Store the {struct} inductive type in native fixpoint AST. | Pierre-Marie Pédrot | 2018-07-13 |
| | | | | | | |||
| | | * | | | Pass a proper environment to Nativelambda.lambda_of_constr. | Pierre-Marie Pédrot | 2018-07-13 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | No need to roll up a new data structure when Environment has O(log n) add and lookup of rel definitions. | ||
| * | | | | | Fixed typos, wording and grammar errors in the Preamble of the Reference ↵ | Zeimer | 2018-07-12 |
| | | | | | | | | | | | | | | | | | | | | | | | | Manual (Introduction, Credits). | ||
* | | | | | | 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 |
|\ \ \ \ \ \ | |_|/ / / / |/| | | | | | |||
| | | | | * | [dev] Autogenerate OCaml dev files. | Emilio Jesus Gallego Arias | 2018-07-12 |
| |_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For now we only copy the templates, but we could do more fancy stuff. This helps to be compatible with build systems that take care of these files automatically, see: https://github.com/coq/coq/pull/6857#discussion_r202096579 | ||
* | | | | | 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 | 2018-07-12 |
| | | | | | | | | | | | | | | | | | | | | See https://github.com/ocaml/num/issues/9 | ||
| | | * | | [warnings] Disable warning 59 [assignment to a non-mutable value] to make ↵ | Emilio Jesus Gallego Arias | 2018-07-12 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | flambda happy. See issue #8043. Using `[@@@ocaml.warning "-59"]` to disable this fails, it seems like an OCaml bug. | ||
| | | * | | [ci] Remove warning jobs in favor of default `-warn-error yes` | Emilio Jesus Gallego Arias | 2018-07-12 |
| |_|/ / |/| | | | | | | | | | | | | | | | As discussed in #6930, we remove the warnings jobs and instead do require the developers to submit a clean build. | ||
* | | | | 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 | 2018-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.0 | Emilio Jesus Gallego Arias | 2018-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. | 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 | 2018-07-11 |
|\ \ \ | | | | | | | | | | | | | the manual | ||
* \ \ \ | 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 | 2018-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 ↵ | 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. | ||
| | | | | | * | | 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 | 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 |
|\ \ \ \ \ \ \ |