aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/Value.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/hls/Value.v')
-rw-r--r--src/hls/Value.v3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/hls/Value.v b/src/hls/Value.v
index d6a3d8b..0d3ea66 100644
--- a/src/hls/Value.v
+++ b/src/hls/Value.v
@@ -1,4 +1,4 @@
-(*
+(*(*
* Vericert: Verified high-level synthesis.
* Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
*
@@ -549,3 +549,4 @@ Proof.
apply Nat2Z.inj_lt in H2.
assumption.
Qed.
+*)