Skip to content
GitLab

Fix ssreflect warning on Coq 8.10

Merged Paolo G. Giarrusso requested to merge Blaisorblade/iris:fix-ssr-warning-810 into master

Since Coq 8.10, move => {}e means move => {e}e. For the backward-compatible syntax and discussion, see https://github.com/coq/coq/issues/10550#issuecomment-542397265.