diff options
Diffstat (limited to 'lib/coq/Sail2_values.v')
| -rw-r--r-- | lib/coq/Sail2_values.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 824ad2d4..e7e4c30b 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1061,8 +1061,8 @@ Ltac unbool_comparisons_goal := | |- context [generic_eq _ _ = false] => apply generic_eq_false | |- context [generic_neq _ _ = true] => apply generic_neq_true | |- context [generic_neq _ _ = false] => apply generic_neq_false - | |- context [_ <> true] => rewrite Bool.not_true_iff_false - | |- context [_ <> false] => rewrite Bool.not_false_iff_true + | |- context [_ <> true] => setoid_rewrite Bool.not_true_iff_false + | |- context [_ <> false] => setoid_rewrite Bool.not_false_iff_true end. (* Split up dependent pairs to get at proofs of properties *) |