aboutsummaryrefslogtreecommitdiffstats
path: root/unit-tests/Tests_lfsc.v
diff options
context:
space:
mode:
Diffstat (limited to 'unit-tests/Tests_lfsc.v')
-rw-r--r--unit-tests/Tests_lfsc.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/unit-tests/Tests_lfsc.v b/unit-tests/Tests_lfsc.v
index 05a9fb4..c868864 100644
--- a/unit-tests/Tests_lfsc.v
+++ b/unit-tests/Tests_lfsc.v
@@ -15,6 +15,8 @@ Add Rec LoadPath "../src" as SMTCoq.
Require Import SMTCoq.
Require Import Bool PArray Int63 List ZArith Logic.
+Local Open Scope Z_scope.
+
Infix "-->" := implb (at level 60, right associativity) : bool_scope.