diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-05 15:24:38 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-05 15:24:38 +0000 |
| commit | 41138b8f14d17f3c409d592c18e5a4def664a2e8 (patch) | |
| tree | 53e61dcd72940f85a085c51d5dc579ffa84a0d86 /theories/MSets/MSetAVL.v | |
| parent | f4ceaf2ce34c5cec168275dee3e7a99710bf835f (diff) | |
Avoid declaring hints about refl/sym/trans of eq in DecidableType2
This used to be convenient in FSets, but since we now try to integrate
DecidableType and OrderedType as foundation for other part of the stdlib,
this should be avoided, otherwise some eauto take a _long_ time.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12626 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/MSets/MSetAVL.v')
| -rw-r--r-- | theories/MSets/MSetAVL.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index 56186e623..c08f46294 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -581,6 +581,10 @@ Hint Unfold lt_tree gt_tree. Hint Resolve @ok. Hint Constructors Ok. +(* TODO: modify proofs in order to avoid these hints *) +Hint Resolve MX.eq_refl MX.eq_trans. +Hint Immediate MX.eq_sym. + Tactic Notation "factornode" ident(l) ident(x) ident(r) ident(h) "as" ident(s) := set (s:=Node l x r h) in *; clearbody s; clear l x r h. |