aboutsummaryrefslogtreecommitdiffstats
path: root/src/verilog/Value.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/verilog/Value.v')
-rw-r--r--src/verilog/Value.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index 2718a46..af2b822 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -468,7 +468,7 @@ Qed.
Lemma ZToValue_eq :
forall w1,
- (mkvalue 32 w1) = (ZToValue 32 (wordToZ w1)). Admitted.
+ (mkvalue 32 w1) = (ZToValue 32 (wordToZ w1)). Abort.
Lemma wordsize_32 :
Int.wordsize = 32%nat.