From c9931180560b7b343427811be0f14281bc791bda Mon Sep 17 00:00:00 2001 From: msozeau Date: Sun, 13 Mar 2011 14:41:09 +0000 Subject: - Add modulo_delta_types flag for unification to allow full conversion when checking types of instanciations while having restricted delta reduction for unification itself. This makes auto/eauto... backward compatible. - Change semantics of [Instance foo : C a.] to _not_ search for an instance of [C a] automatically and potentially slow down interaction, except for trivial classes with no fields. Use [C a := _.] or [C a := {}] to search for an instance of the class or for every field. - Correct treatment of transparency information for classes declared in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13908 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Structures/EqualitiesFacts.v | 8 ++++---- theories/Structures/OrdersFacts.v | 2 +- theories/Structures/OrdersLists.v | 6 +++--- 3 files changed, 8 insertions(+), 8 deletions(-) (limited to 'theories/Structures') diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v index d8a1b7581..c69885b46 100644 --- a/theories/Structures/EqualitiesFacts.v +++ b/theories/Structures/EqualitiesFacts.v @@ -29,9 +29,9 @@ Module KeyDecidableType(Import D:DecidableType). (* eqk, eqke are equalities, ltk is a strict order *) - Global Instance eqk_equiv : Equivalence eqk. + Global Instance eqk_equiv : Equivalence eqk := _. - Global Instance eqke_equiv : Equivalence eqke. + Global Instance eqke_equiv : Equivalence eqke := _. (* Additionnal facts *) @@ -143,7 +143,7 @@ Module PairDecidableType(D1 D2:DecidableType) <: DecidableType. Definition eq := (D1.eq * D2.eq)%signature. - Instance eq_equiv : Equivalence eq. + Instance eq_equiv : Equivalence eq := _. Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. Proof. @@ -159,7 +159,7 @@ End PairDecidableType. Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType. Definition t := (D1.t * D2.t)%type. Definition eq := @eq t. - Program Instance eq_equiv : Equivalence eq. + Instance eq_equiv : Equivalence eq := _. Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. Proof. intros (x1,x2) (y1,y2); diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index a28b79776..b328ae2e8 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -208,7 +208,7 @@ Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull. Definition t := O.t. Definition eq := O.eq. -Instance eq_equiv : Equivalence eq. +Program Instance eq_equiv : Equivalence eq. Definition eq_dec := O.eq_dec. Definition lt := flip O.lt. diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v index 2ed070268..f83b63779 100644 --- a/theories/Structures/OrdersLists.v +++ b/theories/Structures/OrdersLists.v @@ -86,11 +86,11 @@ Module KeyOrderedType(Import O:OrderedType). (* eqk, eqke are equalities, ltk is a strict order *) - Global Instance eqk_equiv : Equivalence eqk. + Global Instance eqk_equiv : Equivalence eqk := _. - Global Instance eqke_equiv : Equivalence eqke. + Global Instance eqke_equiv : Equivalence eqke := _. - Global Instance ltk_strorder : StrictOrder ltk. + Global Instance ltk_strorder : StrictOrder ltk := _. Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk. Proof. unfold eqk, ltk; auto with *. Qed. -- cgit v1.2.3