diff options
Diffstat (limited to 'src/classes/SMT_classes_instances.v')
| -rw-r--r-- | src/classes/SMT_classes_instances.v | 13 |
1 files changed, 2 insertions, 11 deletions
diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v index d6180a0..55e689d 100644 --- a/src/classes/SMT_classes_instances.v +++ b/src/classes/SMT_classes_instances.v @@ -10,9 +10,9 @@ (**************************************************************************) -Require Import Bool OrderedType BinPos ZArith. +Require Import Bool OrderedType BinPos ZArith OrderedTypeEx. Require Import Int63. -Require Import State BVList. +Require Import State BVList FArray. Require Structures. Require Export SMT_classes. @@ -119,8 +119,6 @@ End Bool. Section Z. - Require Import OrderedTypeEx. - Instance Z_ord : OrdType Z. Proof. exists Z_as_OT.lt. @@ -252,8 +250,6 @@ End Z. Section Nat. - Require Import OrderedTypeEx. - Instance Nat_ord : OrdType nat. Proof. @@ -291,9 +287,6 @@ End Nat. Section Positive. - - Require Import OrderedTypeEx. - Instance Positive_ord : OrdType positive. Proof. exists Positive_as_OT.lt. @@ -412,8 +405,6 @@ End BV. Section FArray. - Require Import FArray. - Instance FArray_ord key elt `{key_ord: OrdType key} `{elt_ord: OrdType elt} |