aboutsummaryrefslogtreecommitdiffstats
path: root/src/classes/SMT_classes_instances.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/classes/SMT_classes_instances.v')
-rw-r--r--src/classes/SMT_classes_instances.v3
1 files changed, 1 insertions, 2 deletions
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.