From 8fd9ec8999dd72dd3777a569fdb9cb6f377e2962 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Wed, 28 Apr 2021 14:29:20 +0200
Subject: [PATCH] fix solve_bitvector_eq
---
theories/bitvector.v | 7 +++----
1 file changed, 3 insertions(+), 4 deletions(-)
diff --git a/theories/bitvector.v b/theories/bitvector.v
index b5fd0bb8..69515089 100644
--- a/theories/bitvector.v
+++ b/theories/bitvector.v
@@ -358,16 +358,15 @@ Qed.
(** * Notation for [bv n] *)
Ltac solve_bitvector_eq :=
- try (vm_compute; done);
+ try (vm_compute; exact (conj eq_refl eq_refl));
lazymatch goal with
- | |- -1 < ?v < 2 ^ ?l =>
- fail "Bitvector constant" v "does not fit into" l "bits"
+ |- bv_wf ?n ?v =>
+ fail "Bitvector constant" v "does not fit into" n "bits"
end.
Notation "'[BV{' l } v ]" := (BV l v _) (at level 9, only printing) : stdpp_scope.
(* TODO: Somehow the following version creates a warning. *)
(* Notation "'[BV{' l } v ]" := (BV l v _) (at level 9, format "[BV{ l } v ]", only printing) : stdpp_scope. *)
-(* TODO: This notation breaks when used in gmap notations. Why? *)
Notation "'[BV{' l } v ]" := (BV l v ltac:(solve_bitvector_eq)) (at level 9, only parsing) : stdpp_scope.
(** * Automation *)
--
GitLab