diff options
Diffstat (limited to 'common/Globalenvs.v')
| -rw-r--r-- | common/Globalenvs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/common/Globalenvs.v b/common/Globalenvs.v index f424a69d..1c5bf4ff 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -39,9 +39,9 @@ Require Import Zwf. Require Import Axioms Coqlib Errors Maps AST Linking. Require Import Integers Floats Values Memory. +Declare Scope pair_scope. Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. - Local Open Scope pair_scope. Local Open Scope error_monad_scope. |