Coq: termination measures for mutually recursive functions

1 files changed, 4 insertions, 4 deletions

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