aboutsummaryrefslogtreecommitdiffstats
path: root/src/State.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/State.v')
-rw-r--r--src/State.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/State.v b/src/State.v
index fde25f9..6d31977 100644
--- a/src/State.v
+++ b/src/State.v
@@ -13,6 +13,7 @@
(* *)
(**************************************************************************)
+
Require Import List.
Require Import Bool.
Require Import Int63.
@@ -267,6 +268,7 @@ Module C.
| _ => false
end.
+
Section OR.
Variable or : t -> t -> t.