summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/coq/Primitives.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index d462715f..71a2d9c3 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/Primitives.v
@@ -213,7 +213,6 @@ Proof.
pose (scalar_max_cons_valid ty).
lia.
Qed.
-Print scalar_le_max_valid.
Definition scalar_in_bounds (ty: scalar_ty) (x: Z) : bool :=
scalar_ge_min ty x && scalar_le_max ty x .