Skip to content
Snippets Groups Projects
Commit 1c8bd167 authored by Michael Sammler's avatar Michael Sammler
Browse files

Fix tests for coq#17648

parent 47756278
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
tests/bitvector.ref
+ 0
− 5
View file @ 1c8bd167
...@@ -6,11 +6,6 @@ The command has indeed failed with message: ...@@ -6,11 +6,6 @@ The command has indeed failed with message:
The term "BV 10 5" has type "bv 10" while it is expected to have type "bv 2". The term "BV 10 5" has type "bv 10" while it is expected to have type "bv 2".
BV 2 3 = BV 10 5 BV 2 3 = BV 10 5
: Prop : Prop
The command has indeed failed with message:
Unable to satisfy the following constraints:
?bv_is_wf : "BvWf 2 4"
"bvn_to_bv_test" "bvn_to_bv_test"
: string : string
1 goal 1 goal
......
tests/bitvector.v
+ 0
− 1
View file @ 1c8bd167
...@@ -5,7 +5,6 @@ Check "notation_test". ...@@ -5,7 +5,6 @@ Check "notation_test".
Check (BV 10 3 = BV 10 5). Check (BV 10 3 = BV 10 5).
Fail Check (BV 2 3 = BV 10 5). Fail Check (BV 2 3 = BV 10 5).
Check (BV 2 3 =@{bvn} BV 10 5). Check (BV 2 3 =@{bvn} BV 10 5).
Fail Goal (BV 2 4 = BV 2 3).
Check "bvn_to_bv_test". Check "bvn_to_bv_test".
Goal bvn_to_bv 2 (BV 2 3) = Some (BV 2 3). Proof. simpl. Show. done. Abort. Goal bvn_to_bv 2 (BV 2 3) = Some (BV 2 3). Proof. simpl. Show. done. Abort.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment