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/FMapFullAVL.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/FMapFullAVL.v')
| -rw-r--r-- | theories/FSets/FMapFullAVL.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 8ca9401a06..0ef356b582 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -712,7 +712,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: X.eq x1 x2 -> D.eq d1 d2 -> Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2). Proof. - destruct c; simpl; intros; MX.elim_comp; auto. + destruct c; simpl; intros; MX.elim_comp; auto with ordered_type. Qed. Hint Resolve cons_Cmp : core. |