diff options
Diffstat (limited to 'theories/MSets/MSetRBT.v')
| -rw-r--r-- | theories/MSets/MSetRBT.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index b838495f9..92ad2fcfb 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -452,7 +452,7 @@ 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 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. |