From 46ab3659dd1f2e4839064cfabc03bd19268fa44b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 30 Mar 2018 14:47:06 +0200
Subject: Adapting standard library to the introduction of "Declare Scope".

Removing in passing two Local which are no-ops in practice.
---
 plugins/ssrmatching/ssrmatching.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'plugins/ssrmatching')

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.
-- 
cgit v1.2.3