From 788406cac443d2d33345c0b9db86577c6b39011e Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Tue, 24 Nov 2020 17:04:26 +0100
Subject: Main part of postpasssch proof now completed

---
 aarch64/Asmblock.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'aarch64/Asmblock.v')

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
 
-- 
cgit