| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | Fix #7291: unify tactic should have more descriptive error messages. | Pierre-Marie Pédrot | |
| We simply reuse the same exception as the pretyper instead of raising the generic failure exception in Tactics.unify. | |||
| 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-15 | Use GitHub as the location for OCaml sources. | Théo Zimmermann | |
| It will be more robust and more secure than downloading from the OCaml website. | |||
| 2018-07-14 | [build] Build Coq and plugins with `-strict-sequence` | Emilio Jesus Gallego Arias | |
| Fixes #8067. This is becoming the default in many developments, so it makes sense to require it too, both for Coq and for Plugins. | |||
| 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 | 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 | |
| We turn all Coq warnings that are on by default into errors. | |||
| 2018-07-13 | Generate type-specific code for is_accu in native compilation of fixpoints. | Pierre-Marie Pédrot | |
| This is much more efficient than using Nativevalues.is_accu function which incurs a lot of irrelevant checks on its argument. | |||
| 2018-07-13 | 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 | |
| No need to roll up a new data structure when Environment has O(log n) add and lookup of rel definitions. | |||
| 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 | [dev] Autogenerate OCaml dev files. | Emilio Jesus Gallego Arias | |
| 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 | |||
| 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 | Fix #7854: Native compilation + flambda trigger SEGFAULT. | Pierre-Marie Pédrot | |
| We use a more abstract representation for accumulators in the native compilation scheme, that requires less fiddling with low-level implementation details. It might be slower though. | |||
| 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 | Cleanup reduction effects: they only work on constants. | Gaëtan Gilbert | |
| We only ever call `reduction_effect_hook` on constants, so there's no point allowing it to be declared with globrefs. There is also no point using a constr map instead of constant map. (Technically there was a call of the effect hook on projections, but that can never match a globref so it was useless) | |||
| 2018-07-12 | Statically typecheck the VERNAC EXTEND wrapper. | Pierre-Marie Pédrot | |
| This moves the typing code from the macro expansion to the extension registering mechanism, bringing in more static safety. We also seize the opportunity to remove dead code in the macro. | |||
| 2018-07-12 | Export a wrapper simplifying the registration of vernacular commands. | Pierre-Marie Pédrot | |
| 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 | Export a function to apply toplevel tactic values in Tacinterp. | Pierre-Marie Pédrot | |
| This is a function that keeps beeing asked or reimplemented. It doesn't hurt adding it to the Ltac API. | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |