diff options
| author | msozeau | 2011-03-13 14:41:09 +0000 |
|---|---|---|
| committer | msozeau | 2011-03-13 14:41:09 +0000 |
| commit | c9931180560b7b343427811be0f14281bc791bda (patch) | |
| tree | d46ad35a87de254eac349db3ff31bcaa2ed985f8 /theories/FSets | |
| parent | c70460837f5158325626b9412d8fa0651340b50f (diff) | |
- 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
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FMapPositive.v | 6 | ||||
| -rw-r--r-- | theories/FSets/FSetCompat.v | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index c81a72f892..2067149494 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -494,9 +494,9 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Definition lt_key (p p':positive*A) := E.lt (fst p) (fst p'). - Global Instance eqk_equiv : Equivalence eq_key. - Global Instance eqke_equiv : Equivalence eq_key_elt. - Global Instance ltk_strorder : StrictOrder lt_key. + Global Program Instance eqk_equiv : Equivalence eq_key. + Global Program Instance eqke_equiv : Equivalence eq_key_elt. + Global Program Instance ltk_strorder : StrictOrder lt_key. Lemma mem_find : forall m x, mem x m = match find x m with None => false | _ => true end. diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v index c3d614eebc..6b3d86d398 100644 --- a/theories/FSets/FSetCompat.v +++ b/theories/FSets/FSetCompat.v @@ -264,7 +264,7 @@ Module Update_WSets Instance In_compat : Proper (E.eq==>Logic.eq==>iff) In. Proof. intros x x' Hx s s' Hs. subst. apply MF.In_eq_iff; auto. Qed. - Instance eq_equiv : Equivalence eq. + Instance eq_equiv : Equivalence eq := _. Section Spec. Variable s s': t. |