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

(limited to 'plugins/romega')

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 51b99b9935..da86f4274d 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -8,6 +8,7 @@
  *************************************************************************)
 
 Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable ZArith_base.
+Declare Scope Int_scope.
 Delimit Scope Int_scope with I.
 
 (** * Abstract Integers. *)
@@ -716,6 +717,7 @@ Inductive term : Set :=
   | Topp : term -> term
   | Tvar : N -> term.
 
+Declare Scope romega_scope.
 Bind Scope romega_scope with term.
 Delimit Scope romega_scope with term.
 Arguments Tint _%I.
-- 
cgit v1.2.3