diff options
| author | Brian Campbell | 2018-07-07 23:30:45 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-07-09 13:08:05 +0100 |
| commit | 0ebe1cc6e52ccc28b8629b0cdfa4a00ed1b60988 (patch) | |
| tree | 5667a5ec616a348f2b44fc2c2dcc7336761b1962 /lib | |
| parent | 2c1dfb042ecc10c0ca7868ab186ff8235926d8d3 (diff) | |
Bits for bits of aarch64 in coq
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index ee193865..d18b17bb 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -928,6 +928,7 @@ Ltac unbool_comparisons := | H:context [Z.ltb _ _ = false] |- _ => rewrite Z.ltb_ge in H | H:context [Z.eqb _ _ = false] |- _ => rewrite Z.eqb_neq in H | H:context [orb _ _ = true] |- _ => rewrite Bool.orb_true_iff in H + | H:context [andb _ _ = true] |- _ => apply andb_prop in H | H:context [generic_eq _ _ = true] |- _ => apply generic_eq_true in H | H:context [generic_eq _ _ = false] |- _ => apply generic_eq_false in H | H:context [generic_neq _ _ = true] |- _ => apply generic_neq_true in H |