diff options
| -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. |