diff options
| author | Pierre-Marie Pédrot | 2019-10-04 17:59:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-04 17:59:20 +0200 |
| commit | d5f2e13e51c3404d326f04513a50d264790a7a4c (patch) | |
| tree | 7682460a0831a761fa61cc08b3e5adc324d2b585 /theories/FSets/FSetBridge.v | |
| parent | a8ab4cc9bfa9d31ac08b0ae3e3f318578ce50e2a (diff) | |
| parent | 94f1cb115b791a36ee660e94bf086e1638acbb88 (diff) | |
Merge PR #9772: [Stdlib] OrderedType: do not pollute the “core” hint database
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'theories/FSets/FSetBridge.v')
| -rw-r--r-- | theories/FSets/FSetBridge.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 6e08c38a49..f0b31e6986 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -63,11 +63,11 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. {s' : t | forall y : elt, In y s' <-> ~ E.eq x y /\ In y s}. Proof. intros; exists (remove x s); intuition. - absurd (In x (remove x s)); auto with set. - apply In_1 with y; auto. + absurd (In x (remove x s)); auto with set ordered_type. + apply In_1 with y; auto with ordered_type. elim (E.eq_dec x y); intros; auto. - absurd (In x (remove x s)); auto with set. - apply In_1 with y; auto. + absurd (In x (remove x s)); auto with set ordered_type. + apply In_1 with y; auto with ordered_type. eauto with set. Qed. @@ -470,7 +470,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Hint Resolve elements_3 : core. Lemma elements_3w : forall s : t, NoDupA E.eq (elements s). - Proof. auto. Qed. + Proof. auto with ordered_type. Qed. Definition min_elt (s : t) : option elt := match min_elt s with |