diff options
Diffstat (limited to 'lib/coq/Prompt.v')
| -rw-r--r-- | lib/coq/Prompt.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/lib/coq/Prompt.v b/lib/coq/Prompt.v index 718b2f47..6167f5b7 100644 --- a/lib/coq/Prompt.v +++ b/lib/coq/Prompt.v @@ -1,6 +1,7 @@ Require Import Sail.Values. Require Import Sail.Prompt_monad. Require Export ZArith.Zwf. +Require Import Lia. Require Import List. Import ListNotations. Local Open Scope Z. @@ -169,7 +170,7 @@ refine (Acc_inv _acc _). destruct H. unbool_comparisons. red. -omega. +lia. Defined. (* A version of well-foundedness of measures with a guard to ensure that |