diff options
Diffstat (limited to 'examples/Example.v')
| -rw-r--r-- | examples/Example.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/examples/Example.v b/examples/Example.v index e4a50da..806cd57 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -18,6 +18,7 @@ Require Import SMTCoq.SMTCoq. Require Import Bool. +Require Import ZArith. Local Open Scope Z_scope. Import BVList.BITVECTOR_LIST. @@ -26,6 +27,7 @@ Local Open Scope bv_scope. Import FArray. Local Open Scope farray_scope. +Local Open Scope int63_scope. (* Examples that check ZChaff certificates *) |