The "( X in t )" hack used in the syntax of ssr rewrite may be only p…

…arsing.

This is the only notation to date which breaks the heuristics of
prefering the more precise notations for printing (see #12986).

theories/ssrmatching/ssrmatching.v

@@ -25,7 +25,7 @@ Declare Scope ssrpatternscope.
 Delimit Scope ssrpatternscope with pattern.
 
 (* Notation to define shortcuts for the "X in t" part of a pattern.           *)
-Notation "( X 'in' t )" := (_ : fun X => t) : ssrpatternscope.
+Notation "( X 'in' t )" := (_ : fun X => t) (only parsing) : ssrpatternscope.
 
 (* Some shortcuts for recurrent "X in t" parts.                               *)
 Notation RHS := (X in _ = X)%pattern.