From a88e3b3b6ad01a9b85c828b9a1225732275affee Mon Sep 17 00:00:00 2001 From: ckeller Date: Mon, 11 Mar 2019 20:25:35 +0100 Subject: 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 --- src/classes/SMT_classes_instances.v | 13 ++----------- 1 file changed, 2 insertions(+), 11 deletions(-) (limited to 'src/classes') 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} -- cgit