The following proof script triggers a warning since Rocq 9.2:
From Stdlib Require ssreflect.
Lemma test (P Q R : Prop) : (P -> R) /\ (Q -> R).
Proof.
split; [idtac|] => H.
Warning: In ltac_expr, tolerating this expression at a higher level than expected by the notation continuing on the right. This
tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed.
[level-tolerance,deprecated-since-9.2,deprecated,parsing,default]
We use this pattern around 50 times across std++ and Iris. It is very convenient to be able to introduce some assumptions in each branch of a case distinction.
Is this truly meant to error eventually? Adding parenthesis would look like (split; [idtac|]) => H which doesn't work very well for tactics. Could this be resolved by adjusting the parsing levels of some ltac notations?
Cc @robbertkrebbers
The following proof script triggers a warning since Rocq 9.2:
We use this pattern around 50 times across std++ and Iris. It is very convenient to be able to introduce some assumptions in each branch of a case distinction.
Is this truly meant to error eventually? Adding parenthesis would look like
(split; [idtac|]) => Hwhich doesn't work very well for tactics. Could this be resolved by adjusting the parsing levels of some ltac notations?Cc @robbertkrebbers