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.
---
 theories/Program/Utils.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'theories/Program/Utils.v')

diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index 78c36dc7d1..c51cacac68 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -20,12 +20,13 @@ Notation "{ ( x , y )  :  A  |  P }" :=
   (sig (fun anonymous : A => let (x,y) := anonymous in P))
   (x ident, y ident, at level 10) : type_scope.
 
+Declare Scope program_scope.
+Delimit Scope program_scope with prg.
+
 (** Generates an obligation to prove False. *)
 
 Notation " ! " := (False_rect _ _) : program_scope.
 
-Delimit Scope program_scope with prg.
-
 (** Abbreviation for first projection and hiding of proofs of subset objects. *)
 
 Notation " `  t " := (proj1_sig t) (at level 10, t at next level) : program_scope.
-- 
cgit v1.2.3