From 5dec4b189dd7775229199de11e4c81551b7baaf6 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Mon, 22 Jun 2020 08:12:37 +0200
Subject: restauring Coq compilation with STUBS

---
 kvx/lib/PseudoAsmblock.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'kvx/lib/PseudoAsmblock.v')

diff --git a/kvx/lib/PseudoAsmblock.v b/kvx/lib/PseudoAsmblock.v
index 336e315c..b33ea1bd 100644
--- a/kvx/lib/PseudoAsmblock.v
+++ b/kvx/lib/PseudoAsmblock.v
@@ -27,10 +27,16 @@ Module Pregmap := EMap(PregEq).
 
 Definition regset := Pregmap.t val.
 
+Module AsmNotations.
+
 (* Declare Scope asm. *)
 Notation "a # b" := (a b) (at level 1, only parsing) : asm.
 Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
+Open Scope asm.
+
+End AsmNotations.
 
+Import AsmNotations.
 
 Definition to_Machrs (rs: regset): Mach.regset :=
  fun (r:mreg) => rs r.
@@ -44,7 +50,6 @@ Definition set_from_Machrs (mrs: Mach.regset) (rs: regset): regset :=
    end.
 
 Local Open Scope option_monad_scope.
-Local Open Scope asm.
 
 Record state: Type := State { _rs: regset; _m: mem }.
 Definition outcome := option state.
-- 
cgit