diff options
| author | Hugo Herbelin | 2020-11-06 04:57:46 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-06 05:06:09 +0100 |
| commit | c470b92b8d61fc52b1d7e8697efd36a75ddec9d1 (patch) | |
| tree | 76fb7d4fb407467557c1a2dc21233cf679097d16 | |
| parent | d276a494d29ea69c6a60b16da5dddb9d39f287ca (diff) | |
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).
| -rw-r--r-- | theories/ssrmatching/ssrmatching.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |