From e4a667a4503de1ebda52aee4aa5e08fb0711f1ce Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 18 Jul 2010 11:29:23 +0000 Subject: Tentative de suppression de l'import automatique des hints et coercions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13293 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Structures/GenericMinMax.v | 1 + theories/Structures/OrderedType.v | 1 + theories/Structures/Orders.v | 2 ++ theories/Structures/OrdersFacts.v | 2 ++ theories/Structures/OrdersTac.v | 7 +++++-- 5 files changed, 11 insertions(+), 2 deletions(-) (limited to 'theories/Structures') diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index 68f201897..3b7dea5e4 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -7,6 +7,7 @@ (***********************************************************************) Require Import Orders OrdersTac OrdersFacts Setoid Morphisms Basics. +Import Morphisms_Prop. (* For Hints *) (** * A Generic construction of min and max *) diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index 6b9007fdd..5919a7646 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -7,6 +7,7 @@ (***********************************************************************) Require Export SetoidList Morphisms OrdersTac. +Import Morphisms_Prop. (* For Hints *) Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index f83e77ed8..01c6c62e7 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -7,6 +7,8 @@ (***********************************************************************) Require Export Relations Morphisms Setoid Equalities. +Import Morphisms_Prop. (* For Hints *) + Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index a28b79776..69a7c3b9e 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -8,6 +8,7 @@ Require Import Basics OrdersTac. Require Export Orders. +Import Morphisms_Prop. (* For Hints *) Set Implicit Arguments. Unset Strict Implicit. @@ -206,6 +207,7 @@ End OrderedTypeTest. Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull. +Import O. Definition t := O.t. Definition eq := O.eq. Instance eq_equiv : Equivalence eq. diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v index 66a672c92..80871d102 100644 --- a/theories/Structures/OrdersTac.v +++ b/theories/Structures/OrdersTac.v @@ -87,6 +87,7 @@ Ltac subst_eqns := Definition interp_ord o := match o with OEQ => O.eq | OLT => O.lt | OLE => O.le end. Local Notation "#" := interp_ord. +Import Morphisms_Prop. (* For Hints *) Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z. Proof. @@ -267,19 +268,21 @@ End OT_to_OrderTac. Module TotalOrderRev (O:TotalOrder) <: TotalOrder. +Import O. Definition t := O.t. Definition eq := O.eq. Definition lt := flip O.lt. Definition le := flip O.le. Include EqLtLeNotation. +Import RelationClasses. (* For hints *) (* No Instance syntax to avoid saturating the Equivalence tables *) Definition eq_equiv := O.eq_equiv. Instance lt_strorder: StrictOrder lt. -Proof. unfold lt; auto with *. Qed. +Proof. unfold lt. auto using O.lt_strorder with *. Qed. Instance lt_compat : Proper (eq==>eq==>iff) lt. -Proof. unfold lt; auto with *. Qed. +Proof. unfold lt; auto using O.lt_compat with *. Qed. Lemma le_lteq : forall x y, x<=y <-> x