From 0bf4c8582574b9c7bea43547d75b87c85fdee1e1 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 4 Nov 2020 22:40:19 +0100 Subject: Smart scheduler build problem and flatten solution OK --- aarch64/Asmblock.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'aarch64/Asmblock.v') diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 27292234..4bc56a05 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -336,6 +336,13 @@ Inductive basic : Type := *) . +Inductive instruction : Type := + | PBasic (i: basic) + | PControl (i: control). + +Coercion PBasic: basic >-> instruction. +Coercion PControl: control >-> instruction. + (** * Definition of a bblock A bblock must contain at least one instruction. -- cgit