diff options
| author | Emilio Jesus Gallego Arias | 2018-09-11 11:04:11 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-11 11:04:11 +0200 |
| commit | f3475cd1a68f632b1e6522975354c7dcc1acd6bb (patch) | |
| tree | 6ea45570f34dd67e422b946b0781013692a24709 /plugins/romega | |
| parent | 3dceb51345662b4ceda4214be5ae2d17459f48f3 (diff) | |
| parent | 0aa164f8fc8adf2cd57681ef64ff598c71b5d9f8 (diff) | |
Merge PR #7135: Introducing an explicit `Declare Scope` command
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. |