From 11325d9bb5f4117c5b41413ac523b7d50577ebdd Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 15 Mar 2019 18:42:00 +0000
Subject: Coq: some progress on the test suite Rewrite <> true/false in goals.
 Correct implicits in record and variant types. Use expanded valspecs from the
 type checker in axioms. Allow list notations in type definitions. Skip some
 not-yet-supported tests.

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

(limited to 'lib')

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 *)
-- 
cgit v1.2.3