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 /test-suite | |
| 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 'test-suite')
| -rw-r--r-- | test-suite/bugs/opened/bug_1596.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/test-suite/bugs/opened/bug_1596.v b/test-suite/bugs/opened/bug_1596.v index 820022d995..27cb731151 100644 --- a/test-suite/bugs/opened/bug_1596.v +++ b/test-suite/bugs/opened/bug_1596.v @@ -69,9 +69,8 @@ Definition t := (X.t * Y.t)%type. elim (X.lt_not_eq H2 H3). elim H0;clear H0;intros. right. - split. - eauto. - eauto. + split; + eauto with ordered_type. Qed. Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y). @@ -97,7 +96,7 @@ Definition t := (X.t * Y.t)%type. apply EQ. split;trivial. apply GT. - right;auto. + right;auto with ordered_type. apply GT. left;trivial. Defined. |