From a25181f93604e279b899552b119d68df0c63b0ad Mon Sep 17 00:00:00 2001
From: Valentin Blot <24938579+vblot@users.noreply.github.com>
Date: Thu, 28 Feb 2019 16:20:30 +0100
Subject: Re-fixes in Example.v

---
 examples/Example.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'examples')

diff --git a/examples/Example.v b/examples/Example.v
index 806cd57..b83e619 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -19,7 +19,6 @@ Require Import SMTCoq.SMTCoq.
 Require Import Bool.
 
 Require Import ZArith.
-Local Open Scope Z_scope.
 
 Import BVList.BITVECTOR_LIST.
 Local Open Scope bv_scope.
@@ -27,10 +26,10 @@ Local Open Scope bv_scope.
 Import FArray.
 Local Open Scope farray_scope.
 
-Local Open Scope int63_scope.
-
 (* Examples that check ZChaff certificates *)
 
+Local Open Scope int63_scope.
+
 Zchaff_Checker "sat.cnf" "sat.log".
 Zchaff_Theorem sat "sat.cnf" "sat.log".
 Check sat.
@@ -84,6 +83,8 @@ Proof.
   verit_bool.
 Qed.
 
+Local Open Scope Z_scope.
+
 Goal forall (a b : Z) (P : Z -> bool) (f : Z -> Z),
   (negb (Z.eqb (f a) b)) || (negb (P (f a))) || (P b).
 Proof.
-- 
cgit