From b7374d225af55ecc6f5d6aa8f3684bfae99ff465 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Wed, 2 Oct 2019 19:23:51 +0200 Subject: Make explicit the use of hints from OrderedType (#316) Some hints will move from the core database to the `ordered_type` database (see https://github.com/coq/coq/pull/9772). This commit prepares for this move by adding `with ordered_type` to the invocations of `auto` and `eauto` that use the hints in question. --- lib/Heaps.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'lib/Heaps.v') diff --git a/lib/Heaps.v b/lib/Heaps.v index 9fa07a1d..85343998 100644 --- a/lib/Heaps.v +++ b/lib/Heaps.v @@ -256,14 +256,14 @@ Proof. eapply gt_heap_trans with y; eauto. red; auto. - intuition. eapply lt_heap_trans; eauto. red; auto. - eapply gt_heap_trans; eauto. red; auto. + eapply gt_heap_trans; eauto. red; auto with ordered_type. - intuition. eapply gt_heap_trans; eauto. red; auto. - rewrite e3 in *; simpl in *. intuition. eapply lt_heap_trans with y; eauto. red; auto. eapply gt_heap_trans; eauto. red; auto. - intuition. eapply lt_heap_trans with y; eauto. red; auto. - eapply gt_heap_trans; eauto. red; auto. + eapply gt_heap_trans; eauto. red; auto with ordered_type. eapply gt_heap_trans with x; eauto. red; auto. - rewrite e3 in *; simpl in *; intuition. eapply gt_heap_trans; eauto. red; auto. @@ -308,7 +308,7 @@ Proof. intros. unfold insert. case_eq (partition x h). intros a b EQ; simpl. assert (E.eq y x \/ ~E.eq y x). - destruct (E.compare y x); auto. + destruct (E.compare y x); auto with ordered_type. right; red; intros. elim (E.lt_not_eq l). apply E.eq_sym; auto. destruct H0. tauto. -- cgit