diff options
Diffstat (limited to 'theories/MSets/MSetAVL.v')
| -rw-r--r-- | theories/MSets/MSetAVL.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index db12ee31..e1fc454a 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -38,7 +38,6 @@ Unset Strict Implicit. (* for nicer extraction, we create inductive principles only when needed *) Local Unset Elimination Schemes. -Local Unset Case Analysis Schemes. (** * Ops : the pure functions *) @@ -307,13 +306,13 @@ 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. (* Sometimes functional induction will expose too much of - a tree structure. The following tactic allows to factor back + a tree structure. The following tactic allows factoring back a Node whose internal parts occurs nowhere else. *) (* TODO: why Ltac instead of Tactic Notation don't work ? why clear ? *) |