aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--src/verilog/Verilog.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index c1c68ba..61df580 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -419,7 +419,7 @@ Definition module_run (n : nat) (m : module) : res assoclist :=
Local Close Scope error_monad_scope.
-Theorem value_eq_size_if_eq:
+(*Theorem value_eq_size_if_eq:
forall lv rv EQ,
vsize lv = vsize rv -> value_eq_size lv rv = left EQ.
Proof. intros. unfold value_eq_size.