diff options
Diffstat (limited to 'theories/MSets/MSetGenTree.v')
| -rw-r--r-- | theories/MSets/MSetGenTree.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 901574235..d1d9897fb 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -970,6 +970,8 @@ Definition lt (s1 s2 : tree) : Prop := exists s1' s2', Ok s1' /\ Ok s2' /\ eq s1 s1' /\ eq s2 s2' /\ L.lt (elements s1') (elements s2'). +Declare Equivalent Keys L.eq equivlistA. + Instance lt_strorder : StrictOrder lt. Proof. split. |