diff options
Diffstat (limited to 'theories/MSets/MSetRBT.v')
| -rw-r--r-- | theories/MSets/MSetRBT.v | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index eab01a55b0..f9105fdf74 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -450,13 +450,13 @@ Include MSetGenTree.Props X Color. Local Notation Rd := (Node Red). Local Notation Bk := (Node Black). -Local Hint Immediate MX.eq_sym. -Local Hint Unfold In lt_tree gt_tree Ok. -Local Hint Constructors InT bst. -Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok. -Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node. -Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans. -Local Hint Resolve elements_spec2. +Local Hint Immediate MX.eq_sym : core. +Local Hint Unfold In lt_tree gt_tree Ok : core. +Local Hint Constructors InT bst : core. +Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok : core. +Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core. +Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core. +Local Hint Resolve elements_spec2 : core. (** ** Singleton set *) @@ -1136,7 +1136,7 @@ Record INV l1 l2 acc : Prop := { acc_sorted : sort X.lt acc; l1_lt_acc x y : InA X.eq x l1 -> InA X.eq y acc -> X.lt x y; l2_lt_acc x y : InA X.eq x l2 -> InA X.eq y acc -> X.lt x y}. -Local Hint Resolve l1_sorted l2_sorted acc_sorted. +Local Hint Resolve l1_sorted l2_sorted acc_sorted : core. Lemma INV_init s1 s2 `(Ok s1, Ok s2) : INV (rev_elements s1) (rev_elements s2) nil. @@ -1506,8 +1506,8 @@ Class Rbt (t:tree) := RBT : exists d, rbt d t. (** ** Basic tactics and results about red-black *) Scheme rbt_ind := Induction for rbt Sort Prop. -Local Hint Constructors rbt rrt arbt. -Local Hint Extern 0 (notred _) => (exact I). +Local Hint Constructors rbt rrt arbt : core. +Local Hint Extern 0 (notred _) => (exact I) : core. Ltac invrb := intros; invtree rrt; invtree rbt; try contradiction. Ltac desarb := match goal with H:arbt _ _ |- _ => destruct H end. Ltac nonzero n := destruct n as [|n]; [try split; invrb|]. @@ -1519,7 +1519,7 @@ Proof. destruct l, r; descolor; invrb; auto. Qed. -Local Hint Resolve rr_nrr_rb. +Local Hint Resolve rr_nrr_rb : core. Lemma arb_nrr_rb n t : arbt n t -> notredred t -> rbt n t. @@ -1533,7 +1533,7 @@ Proof. destruct 1; destruct t; descolor; invrb; auto. Qed. -Local Hint Resolve arb_nrr_rb arb_nr_rb. +Local Hint Resolve arb_nrr_rb arb_nr_rb : core. (** ** A Red-Black tree has indeed a logarithmic depth *) |