diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-24 17:04:26 +0100 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-24 17:04:26 +0100 |
commit | 788406cac443d2d33345c0b9db86577c6b39011e (patch) | |
tree | 1790aa8c5b42c9abd89adb8af072f179897fc483 /aarch64/Asmblock.v | |
parent | 1fc20a7262e6de3234e4411ae359b2e4e5ac36ee (diff) | |
download | compcert-kvx-788406cac443d2d33345c0b9db86577c6b39011e.tar.gz compcert-kvx-788406cac443d2d33345c0b9db86577c6b39011e.zip |
Main part of postpasssch proof now completed
Diffstat (limited to 'aarch64/Asmblock.v')
-rw-r--r-- | aarch64/Asmblock.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index da45324b..7f94a087 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -336,12 +336,13 @@ Inductive basic : Type := *) . +(* Not used in Coq, declared in ocaml directly in PostpassSchedulingOracle.ml Inductive instruction : Type := | PBasic (i: basic) | PControl (i: control). Coercion PBasic: basic >-> instruction. -Coercion PControl: control >-> instruction. +Coercion PControl: control >-> instruction. *) (** * Definition of a bblock |