aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/Gible.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/hls/Gible.v')
-rw-r--r--src/hls/Gible.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/hls/Gible.v b/src/hls/Gible.v
index fdc9a9d..0603269 100644
--- a/src/hls/Gible.v
+++ b/src/hls/Gible.v
@@ -43,6 +43,8 @@ Require Import Predicate.
Require Import Vericertlib.
Definition node := positive.
+Definition predicate := positive.
+Definition pred_op := @pred_op predicate.
(*|
.. index::