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/Basics.v | 2 ++
 1 file changed, 2 insertions(+)

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

diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index f55093ed48..c2316689fc 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -28,6 +28,8 @@ Definition compose {A B C} (g : B -> C) (f : A -> B) :=
 
 Hint Unfold compose.
 
+Declare Scope program_scope.
+
 Notation " g ∘ f " := (compose g f)
   (at level 40, left associativity) : program_scope.
 
-- 
cgit v1.2.3