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/FSetProperties.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/FSetProperties.v')
| -rw-r--r-- | theories/FSets/FSetProperties.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index c6b2e0a09d..e500debc73 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -939,7 +939,7 @@ Module OrdProperties (M:S). generalize (gtb_1 x a)(gtb_1 x b); destruct (gtb x a); destruct (gtb x b); auto. intros. symmetry; rewrite H1. - apply ME.eq_lt with a; auto. + apply ME.eq_lt with a; auto with ordered_type. rewrite <- H0; auto. intros. rewrite H0. @@ -1013,7 +1013,7 @@ Module OrdProperties (M:S). intros. inversion_clear H2. rewrite <- elements_iff in H1. - apply ME.lt_eq with x; auto. + apply ME.lt_eq with x; auto with ordered_type. inversion H3. red; intros a. rewrite InA_app_iff, InA_cons, InA_nil by auto with *. @@ -1052,7 +1052,7 @@ Module OrdProperties (M:S). apply X0 with (remove e s) e; auto with set. apply IHn. assert (S n = S (cardinal (remove e s))). - rewrite Heqn; apply cardinal_2 with e; auto with set. + rewrite Heqn; apply cardinal_2 with e; auto with set ordered_type. inversion H0; auto. red; intros. rewrite remove_iff in H0; destruct H0. @@ -1073,7 +1073,7 @@ Module OrdProperties (M:S). apply X0 with (remove e s) e; auto with set. apply IHn. assert (S n = S (cardinal (remove e s))). - rewrite Heqn; apply cardinal_2 with e; auto with set. + rewrite Heqn; apply cardinal_2 with e; auto with set ordered_type. inversion H0; auto. red; intros. rewrite remove_iff in H0; destruct H0. |