Skip to content
Snippets Groups Projects

Enable `Hint Mode Equiv` now that stdpp requires Coq 8.12

Closed Paolo G. Giarrusso requested to merge Blaisorblade/stdpp:mode-equiv into master

Includes fixes for Coq 8.12/8.13 — but we might want to drop those.

Rationale: while Coq bug https://github.com/coq/coq/issues/14441 is still relevant, Iris chose to pay the costs of those annotations. Back then, stdpp didn't because it still supported Coq 8.11 which suffered from additional bugs (fixed in 8.12) — Iris still has this comment:

 (* No Hint Mode set in stdpp because of Coq bugs #5735 and #9058, only
 fixed in Coq >= 8.12, which Iris depends on. *)
Edited by Paolo G. Giarrusso

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
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
Please register or sign in to reply
Loading