From e5d108332cf700f73ea7b7527d0ae6006b0944c5 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 17 Dec 2018 12:23:30 +0000
Subject: Adapt Coq and termination measure support to typechecker changes Also
 output termination measures in Sail printer

---
 lib/coq/Sail2_string.v | 8 ++++----
 lib/coq/Sail2_values.v | 8 ++++----
 2 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v
index a02556b2..0a00f8d7 100644
--- a/lib/coq/Sail2_string.v
+++ b/lib/coq/Sail2_string.v
@@ -7,12 +7,12 @@ Definition string_startswith s expected :=
   let prefix := String.substring 0 (String.length expected) s in
   generic_eq prefix expected.
 
-Definition string_drop s (n : {n : Z & ArithFact (n >= 0)}) :=
-  let n := Z.to_nat (projT1 n) in
+Definition string_drop s (n : Z) `{ArithFact (n >= 0)} :=
+  let n := Z.to_nat n in
   String.substring n (String.length s - n) s.
 
-Definition string_take s (n : {n : Z & ArithFact (n >= 0)}) :=
-  let n := Z.to_nat (projT1 n) in
+Definition string_take s (n : Z) `{ArithFact (n >= 0)} :=
+  let n := Z.to_nat n in
   String.substring 0 n s.
 
 Definition string_length s : {n : Z & ArithFact (n >= 0)} :=
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index aebc3376..37e75961 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1790,11 +1790,11 @@ match a with
 | None => None
 end.
 
-Definition sub_nat (x : {x : Z & ArithFact (x >= 0)}) (y : {y : Z & ArithFact (y >= 0)}) :
+Definition sub_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} :
   {z : Z & ArithFact (z >= 0)} :=
-  let z := projT1 x - projT1 y in
+  let z := x - y in
   if sumbool_of_bool (z >=? 0) then build_ex z else build_ex 0.
 
-Definition min_nat (x : {x : Z & ArithFact (x >= 0)}) (y : {y : Z & ArithFact (y >= 0)}) :
+Definition min_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} :
   {z : Z & ArithFact (z >= 0)} :=
-  build_ex (Z.min (projT1 x) (projT1 y)).
+  build_ex (Z.min x y).
-- 
cgit v1.2.3