diff options
Diffstat (limited to 'plugins/romega')
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 2 |
1 files changed, 2 insertions, 0 deletions
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. |