diff options
| author | ckeller <ckeller@users.noreply.github.com> | 2019-03-11 20:25:35 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-11 20:25:35 +0100 |
| commit | a88e3b3b6ad01a9b85c828b9a1225732275affee (patch) | |
| tree | acc3768695698a80867b4ce941ab4cb7b4b99d7a /src/classes/SMT_classes_instances.v | |
| parent | 33010bfa6345549d8b9b0c06f44150b60d0c86e5 (diff) | |
| download | smtcoq-a88e3b3b6ad01a9b85c828b9a1225732275affee.tar.gz smtcoq-a88e3b3b6ad01a9b85c828b9a1225732275affee.zip | |
V8.8 (#42)
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Organization structures
* 8.8 ok with standard coq
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} |