Skip to content
Snippets Groups Projects

Stop mentioning Coq bug fixed in Coq >= 8.13

Merged Stop mentioning Coq bug fixed in Coq >= 8.13
Blaisorblade/stdpp:revise-readme into master
1 unresolved thread
Merged Paolo G. Giarrusso requested to merge Blaisorblade/stdpp:revise-readme into master
1 unresolved thread

This should wait till stdpp drops support for Coq 8.12, but that's soon IIUC.

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Paolo G. Giarrusso added 14 commits

    added 14 commits

    Compare with previous version

  • Paolo G. Giarrusso added 1 commit

    added 1 commit

    • f1d8b960 - Stop mentioning Coq bug fixed in Coq >= 8.13

    Compare with previous version

  • Paolo G. Giarrusso resolved all threads

    resolved all threads

  • Paolo G. Giarrusso
    Paolo G. Giarrusso @Blaisorblade
    Author Contributor

    New version also tweaked text a bit. Feel free to tweak further.

  • Robbert Krebbers
  • Robbert Krebbers resolved all threads

    resolved all threads

  • Robbert Krebbers merged

    merged

  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers
    Owner

    Merging. Thanks.

  • Robbert Krebbers mentioned in commit d0cfa8a5

    mentioned in commit d0cfa8a5

  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
    • README.md
    26 26 Notably:
    27 27
    28 28 * `Generalizable All Variables`: This option enables implicit generalization in
    29 arguments of the form `` `{...}`` (i.e., anonymous arguments). Unfortunately, it
    30 also enables implicit generalization in `Instance`. We think that the fact
    31 that both behaviors are coupled together is a
    32 [bug in Coq](https://github.com/coq/coq/issues/6030).
    29 arguments of the form `` `{...}`` (i.e., anonymous arguments) and in terms of
    30 shape `` `{}``/`` `[]``/`` `()``. See [Coq's
    31 manual](https://coq.inria.fr/distrib/current/refman/language/extensions/implicit-arguments.html#implicit-generalization)
    32 for further details.
    Please register or sign in to reply