diff options
Diffstat (limited to 'theories/MSets/MSetAVL.v')
| -rw-r--r-- | theories/MSets/MSetAVL.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index 1e66e2b5b..2182504dd 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -306,7 +306,7 @@ Include MSetGenTree.Props X I. 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. |