summaryrefslogtreecommitdiff
path: root/test/builtins/test.v
diff options
context:
space:
mode:
authorBrian Campbell2021-04-23 17:05:13 +0100
committerBrian Campbell2021-04-23 17:05:13 +0100
commit75af862bbbff6797dd4a5dfa38b4bb617b034ac4 (patch)
tree291afb7a36200b8cc01896d59cc27b234ff48f28 /test/builtins/test.v
parent1cb28eeb9289624b6f187705fe20e6176ccf1406 (diff)
Add isla builtin testing and update coq scriptsail2
(both off by default)
Diffstat (limited to 'test/builtins/test.v')
-rw-r--r--test/builtins/test.v3
1 files changed, 1 insertions, 2 deletions
diff --git a/test/builtins/test.v b/test/builtins/test.v
index 64c5bf10..4290d8ff 100644
--- a/test/builtins/test.v
+++ b/test/builtins/test.v
@@ -1,5 +1,4 @@
-Require Import Sail2_state_monad.
-Require Import Sail2_state_lifting.
+From Sail Require Import State_monad State_lifting.
Require Import String.
Require Import List.
Import ListNotations.