diff options
| author | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2019-02-28 16:14:59 +0100 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2019-02-28 16:14:59 +0100 |
| commit | f479497576c11bc0fcc116ede778d1744be6d78e (patch) | |
| tree | 21a5c0a04483fbcd38e5e1a81be2259576f336e2 /examples | |
| parent | d5634a96698a29192d292ce03c7e4b7ff42a411a (diff) | |
| download | smtcoq-f479497576c11bc0fcc116ede778d1744be6d78e.tar.gz smtcoq-f479497576c11bc0fcc116ede778d1744be6d78e.zip | |
Fixes in Example.v
Diffstat (limited to 'examples')
| -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 *) |