Iris shadows ssreflect new syntax
Iris [^
notation shadows (and prevents using) ssreflect's new [^ syntax for "block introductions": move/elim => [^ prefix]
.
Since Coq 8.10.1 ssreflect introduced syntax using [^
and [^~
, but they're shadowed by iris's big_op notations.
Here's a mininal example. Block introductions are pointless here — but useful for big datatypes.
Example (EDIT: updated for modern Iris).
(* https://gitlab.mpi-sws.org/iris/iris/-/issues/273 *)
From iris.prelude Require Import prelude.
Lemma foo (n : nat) : n = n.
elim: n => [^ s]. (* Works *)
Restart.
elim: n => [^~ s]. (* Works *)
Abort.
Locate "[^". (* big_op notations *)
From iris.proofmode Require Import tactics.
Locate "[^". (* big_op notations *)
Lemma foo (n : nat) : n = n.
(* Parse error for each of the following commands: *)
elim: n => [^~ s].
elim: n => [^ s].
(* Each gives:
Syntax error: [tactic:ssripats_ne] expected after '=>' (in [tactic:ssrintros_ne]).
*)
Iris version: dev.2019-11-02.2.ea809ed4 .. 4.0.0