From 40b8a7334da948e7f368defa2b913056d9c55a59 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 28 Jun 2018 13:50:17 +0100
Subject: Fix build of Aarch64_mono.thy

---
 aarch64/mono/aarch64_extras.lem               | 10 +++++-----
 aarch64/mono/demo/aarch64_no_vector/spec.sail |  2 ++
 2 files changed, 7 insertions(+), 5 deletions(-)

(limited to 'aarch64')

diff --git a/aarch64/mono/aarch64_extras.lem b/aarch64/mono/aarch64_extras.lem
index fb1e4861..1e91dd31 100644
--- a/aarch64/mono/aarch64_extras.lem
+++ b/aarch64/mono/aarch64_extras.lem
@@ -1,9 +1,9 @@
 open import Pervasives_extra
-open import Sail_instr_kinds
-open import Sail_values
-open import Sail_operators_mwords
-open import Prompt_monad
-open import Prompt
+open import Sail2_instr_kinds
+open import Sail2_values
+open import Sail2_operators_mwords
+open import Sail2_prompt_monad
+open import Sail2_prompt
 
 type ty512
 instance (Size ty512) let size = 512 end
diff --git a/aarch64/mono/demo/aarch64_no_vector/spec.sail b/aarch64/mono/demo/aarch64_no_vector/spec.sail
index ab68c973..19a06c57 100644
--- a/aarch64/mono/demo/aarch64_no_vector/spec.sail
+++ b/aarch64/mono/demo/aarch64_no_vector/spec.sail
@@ -2064,6 +2064,8 @@ val Replicate : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.
 
 function Replicate x = {
   assert('N % 'M == 0, "((N MOD M) == 0)");
+  let 'O = 'N / 'M;
+  assert(constraint('O * 'M = 'N));
   return(replicate_bits(x, 'N / 'M))
 }
 
-- 
cgit v1.2.3