From 60e9b04db40028d93dfa62792af1dd524e5c6a60 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 15 Jun 2020 14:23:09 +0100 Subject: Update handwritten Coq support files to match current Sail. --- handwritten_support/riscv_extras.v | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'handwritten_support/riscv_extras.v') diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v index 8d7cefc..7537349 100644 --- a/handwritten_support/riscv_extras.v +++ b/handwritten_support/riscv_extras.v @@ -1,11 +1,8 @@ -Require Import Sail2_instr_kinds. -Require Import Sail2_values. -Require Import Sail2_operators_mwords. -Require Import Sail2_prompt_monad. -Require Import Sail2_prompt. +Require Import Sail.Base. Require Import String. Require Import List. Import List.ListNotations. +Open Scope Z. Axiom real : Type. -- cgit v1.1