diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /theories/Structures | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'theories/Structures')
-rw-r--r-- | theories/Structures/DecidableType.v | 20 | ||||
-rw-r--r-- | theories/Structures/DecidableTypeEx.v | 16 | ||||
-rw-r--r-- | theories/Structures/Equalities.v | 16 | ||||
-rw-r--r-- | theories/Structures/EqualitiesFacts.v | 16 | ||||
-rw-r--r-- | theories/Structures/GenericMinMax.v | 16 | ||||
-rw-r--r-- | theories/Structures/OrderedType.v | 16 | ||||
-rw-r--r-- | theories/Structures/OrderedTypeAlt.v | 16 | ||||
-rw-r--r-- | theories/Structures/OrderedTypeEx.v | 18 | ||||
-rw-r--r-- | theories/Structures/Orders.v | 16 | ||||
-rw-r--r-- | theories/Structures/OrdersAlt.v | 16 | ||||
-rw-r--r-- | theories/Structures/OrdersEx.v | 16 | ||||
-rw-r--r-- | theories/Structures/OrdersFacts.v | 16 | ||||
-rw-r--r-- | theories/Structures/OrdersLists.v | 16 | ||||
-rw-r--r-- | theories/Structures/OrdersTac.v | 16 | ||||
-rw-r--r-- | theories/Structures/vo.itarget | 14 |
15 files changed, 129 insertions, 115 deletions
diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v index f85222df..24333ad8 100644 --- a/theories/Structures/DecidableType.v +++ b/theories/Structures/DecidableType.v @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) Require Export SetoidList. Require Equalities. @@ -86,7 +88,7 @@ Module KeyDecidableType(D:DecidableType). Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. Proof. - intros; apply InA_eqA with p; auto with *. + intros; apply InA_eqA with p; auto using eqk_equiv. Qed. Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). @@ -109,7 +111,7 @@ Module KeyDecidableType(D:DecidableType). Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. Proof. - intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *. + intros; unfold MapsTo in *; apply InA_eqA with (x,e); auto using eqke_equiv. Qed. Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. diff --git a/theories/Structures/DecidableTypeEx.v b/theories/Structures/DecidableTypeEx.v index 163a40f2..8dd2e710 100644 --- a/theories/Structures/DecidableTypeEx.v +++ b/theories/Structures/DecidableTypeEx.v @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) Require Import DecidableType OrderedType OrderedTypeEx. Set Implicit Arguments. diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v index 747d03f8..5f60a979 100644 --- a/theories/Structures/Equalities.v +++ b/theories/Structures/Equalities.v @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) Require Export RelationClasses. Require Import Bool Morphisms Setoid. diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v index cee3d63f..7b6ee2ea 100644 --- a/theories/Structures/EqualitiesFacts.v +++ b/theories/Structures/EqualitiesFacts.v @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) Require Import Equalities Bool SetoidList RelationPairs. diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index ac52d1bb..05edc6cc 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) Require Import Orders OrdersTac OrdersFacts Setoid Morphisms Basics. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index 93ca383b..f6fc247d 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) Require Export SetoidList Morphisms OrdersTac. Set Implicit Arguments. diff --git a/theories/Structures/OrderedTypeAlt.v b/theories/Structures/OrderedTypeAlt.v index b054496e..278046a8 100644 --- a/theories/Structures/OrderedTypeAlt.v +++ b/theories/Structures/OrderedTypeAlt.v @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) Require Import OrderedType. (** * An alternative (but equivalent) presentation for an Ordered Type diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v index 3c6afc7b..f2a9a569 100644 --- a/theories/Structures/OrderedTypeEx.v +++ b/theories/Structures/OrderedTypeEx.v @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) Require Import OrderedType. Require Import ZArith. @@ -55,7 +57,7 @@ Module Nat_as_OT <: UsualOrderedType. Definition compare x y : Compare lt eq x y. Proof. - case_eq (nat_compare x y); intro. + case_eq (Nat.compare x y); intro. - apply EQ. now apply nat_compare_eq. - apply LT. now apply nat_compare_Lt_lt. - apply GT. now apply nat_compare_Gt_gt. diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index 724690b4..42756ad3 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) Require Export Relations Morphisms Setoid Equalities. Set Implicit Arguments. diff --git a/theories/Structures/OrdersAlt.v b/theories/Structures/OrdersAlt.v index 5dd917a7..ad6a3876 100644 --- a/theories/Structures/OrdersAlt.v +++ b/theories/Structures/OrdersAlt.v @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) (* Finite sets library. * Authors: Pierre Letouzey and Jean-Christophe FilliĆ¢tre diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v index 89c56388..93168f7d 100644 --- a/theories/Structures/OrdersEx.v +++ b/theories/Structures/OrdersEx.v @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) (* Finite sets library. * Authors: Pierre Letouzey and Jean-Christophe FilliĆ¢tre diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 0115d8a5..87df6b47 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) Require Import Bool Basics OrdersTac. Require Export Orders. diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v index bf8529bc..abdb9eff 100644 --- a/theories/Structures/OrdersLists.v +++ b/theories/Structures/OrdersLists.v @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) Require Export RelationPairs SetoidList Orders EqualitiesFacts. diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v index 475a25a4..ebd8ee8f 100644 --- a/theories/Structures/OrdersTac.v +++ b/theories/Structures/OrdersTac.v @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) Require Import Setoid Morphisms Basics Equalities Orders. Set Implicit Arguments. diff --git a/theories/Structures/vo.itarget b/theories/Structures/vo.itarget deleted file mode 100644 index 674e9fba..00000000 --- a/theories/Structures/vo.itarget +++ /dev/null @@ -1,14 +0,0 @@ -Equalities.vo -EqualitiesFacts.vo -Orders.vo -OrdersEx.vo -OrdersFacts.vo -OrdersLists.vo -OrdersTac.vo -OrdersAlt.vo -GenericMinMax.vo -DecidableType.vo -DecidableTypeEx.vo -OrderedTypeAlt.vo -OrderedTypeEx.vo -OrderedType.vo |