From 889f129b824790694f820d7d083607796abd3efb Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 5 Apr 2019 18:59:01 +0100
Subject: Coq: termination measures for mutually recursive functions

---
 lib/coq/Sail2_prompt.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index bae8381e..8efd66f0 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -129,11 +129,11 @@ wfR) y)
  end.
 
 Definition Zwf_guarded (z:Z) : Acc (Zwf 0) z :=
-  match z with
+  Acc_intro _ (fun y H => match z with
   | Zpos p => pos_guard_wf p (Zwf_well_founded _) _
-  | _ => Zwf_well_founded _ _
-  end.
-
+  | Zneg p => pos_guard_wf p (Zwf_well_founded _) _
+  | Z0 => Zwf_well_founded _ _
+  end).
 
 (*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-- 
cgit v1.2.3