From c470b92b8d61fc52b1d7e8697efd36a75ddec9d1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 6 Nov 2020 04:57:46 +0100
Subject: The "( X in t )" hack used in the syntax of ssr rewrite may be only
 parsing.

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 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/ssrmatching/ssrmatching.v b/theories/ssrmatching/ssrmatching.v
index feca62651d..fda6b860e6 100644
--- a/theories/ssrmatching/ssrmatching.v
+++ b/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.
-- 
cgit v1.2.3