diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_prompt.v | 8 |
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 |