From b96d222d47da5c5d59b65dfa152e255b7a4f7b46 Mon Sep 17 00:00:00 2001
From: Valentin Blot <24938579+vblot@users.noreply.github.com>
Date: Thu, 28 Feb 2019 16:26:11 +0100
Subject: int does not exist in standard coq

---
 examples/Example.v | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/examples/Example.v b/examples/Example.v
index b83e619..5c740d6 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -62,10 +62,7 @@ Proof.
   zchaff.
 Qed.
 
-Goal forall i j k,
-  let a := (i == j)%int in
-  let b := (j == k)%int in
-  let c := (k == i)%int in
+Goal forall a b c,
   (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false.
 Proof.
   zchaff.
-- 
cgit