From e12110637730d067c216abcc86185b761189b342 Mon Sep 17 00:00:00 2001
From: vblot <24938579+vblot@users.noreply.github.com>
Date: Fri, 28 May 2021 18:29:37 +0200
Subject: getting rid of native-coq (#95)

---
 src/classes/SMT_classes_instances.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'src/classes')

diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v
index aa2082e..a2831cf 100644
--- a/src/classes/SMT_classes_instances.v
+++ b/src/classes/SMT_classes_instances.v
@@ -13,7 +13,6 @@
 Require Import Bool OrderedType BinPos ZArith OrderedTypeEx.
 Require Import Int63.
 Require Import State BVList FArray.
-Require Structures.
 Require Export SMT_classes.
 
 
@@ -253,7 +252,7 @@ Section Nat.
   Defined.
 
   Global Instance Nat_eqbtype : EqbType nat :=
-    {| eqb := Structures.nat_eqb; eqb_spec := Structures.nat_eqb_eq |}.
+    {| eqb := Nat.eqb; eqb_spec := Nat.eqb_eq |}.
 
   Global Instance Nat_dec : DecType nat := EqbToDecType.
 
-- 
cgit