diff options
| author | Hugo Herbelin | 2018-03-30 14:47:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-10 13:07:29 +0200 |
| commit | 46ab3659dd1f2e4839064cfabc03bd19268fa44b (patch) | |
| tree | a4b215eb3289a189c9756bf44c3e52d04f306c99 /plugins/ssrmatching | |
| parent | 8e675d70ad1f60cbbf9f1e630ce6dee61347c7ca (diff) | |
Adapting standard library to the introduction of "Declare Scope".
Removing in passing two Local which are no-ops in practice.
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.v b/plugins/ssrmatching/ssrmatching.v index 829ee05e11..9a53e1dd1a 100644 --- a/plugins/ssrmatching/ssrmatching.v +++ b/plugins/ssrmatching/ssrmatching.v @@ -11,9 +11,11 @@ Reserved Notation "( a 'as' b )" (at level 0). Reserved Notation "( a 'in' b 'in' c )" (at level 0). Reserved Notation "( a 'as' b 'in' c )" (at level 0). +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. -Delimit Scope ssrpatternscope with pattern. (* Some shortcuts for recurrent "X in t" parts. *) Notation RHS := (X in _ = X)%pattern. |