diff options
| author | Brian Campbell | 2019-03-15 18:42:00 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-03-15 18:42:09 +0000 |
| commit | 11325d9bb5f4117c5b41413ac523b7d50577ebdd (patch) | |
| tree | ff7bdf38eb6b3b0d2665badac4ac3287629cc188 /lib | |
| parent | c1f9e24213b50fb622ac94f816e304eabc75ba75 (diff) | |
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.
Diffstat (limited to 'lib')
| -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 *) |