diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-06-22 08:12:37 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-06-22 08:12:37 +0200 |
| commit | 5dec4b189dd7775229199de11e4c81551b7baaf6 (patch) | |
| tree | 6ef4f77034cd9003256e34e31e5b91c35a4e1b85 /kvx/lib | |
| parent | 0cde06d359ff8b265b38eef5f62a2e8f4e744059 (diff) | |
| download | compcert-kvx-5dec4b189dd7775229199de11e4c81551b7baaf6.tar.gz compcert-kvx-5dec4b189dd7775229199de11e4c81551b7baaf6.zip | |
restauring Coq compilation with STUBS
Diffstat (limited to 'kvx/lib')
| -rw-r--r-- | kvx/lib/PseudoAsmblock.v | 7 | ||||
| -rw-r--r-- | kvx/lib/PseudoAsmblockproof.v | 2 |
2 files changed, 7 insertions, 2 deletions
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. diff --git a/kvx/lib/PseudoAsmblockproof.v b/kvx/lib/PseudoAsmblockproof.v index 3eb80ebb..67308278 100644 --- a/kvx/lib/PseudoAsmblockproof.v +++ b/kvx/lib/PseudoAsmblockproof.v @@ -52,6 +52,7 @@ End TRANSLATION. *) Require Import Linking. +Import PseudoAsmblock.AsmNotations. Section PRESERVATION. @@ -65,7 +66,6 @@ Proof. Qed. Local Open Scope Z_scope. -Local Open Scope asm. Local Open Scope option_monad_scope. Variable prog: program. |