diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-12 16:54:08 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-12 16:54:08 +0000 |
| commit | 8bfc7b2ac5a4d6d218071611a5002e513e731451 (patch) | |
| tree | 424b2ea522c86f5ab2d156821e625812231df751 /theories/MSets/MSetWeakList.v | |
| parent | b264811fbed75caff5deb2b6eb78a327dc134f68 (diff) | |
MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12656 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/MSets/MSetWeakList.v')
| -rw-r--r-- | theories/MSets/MSetWeakList.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v index feab44f58..6b9c17079 100644 --- a/theories/MSets/MSetWeakList.v +++ b/theories/MSets/MSetWeakList.v @@ -126,17 +126,17 @@ Module MakeRaw (X:DecidableType) <: WRawSets X. Definition IsOk := NoDup. - Class Ok (s:t) : Prop := { ok : NoDup s }. + Class Ok (s:t) : Prop := ok : NoDup s. - Hint Constructors Ok. + Hint Unfold Ok. Hint Resolve @ok. Instance NoDup_Ok s (nd : NoDup s) : Ok s := { ok := nd }. Ltac inv_ok := match goal with - | H:Ok (_ :: _) |- _ => apply @ok in H; inversion_clear H; inv_ok + | H:Ok (_ :: _) |- _ => inversion_clear H; inv_ok | H:Ok nil |- _ => clear H; inv_ok - | H:NoDup ?l |- _ => generalize (Build_Ok H); clear H; intro H; inv_ok + | H:NoDup ?l |- _ => change (Ok l) in H; inv_ok | _ => idtac end. |