From f479497576c11bc0fcc116ede778d1744be6d78e Mon Sep 17 00:00:00 2001
From: Valentin Blot <24938579+vblot@users.noreply.github.com>
Date: Thu, 28 Feb 2019 16:14:59 +0100
Subject: Fixes in Example.v

---
 examples/Example.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'examples/Example.v')

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 *)
 
-- 
cgit