diff options
Diffstat (limited to 'theories/MSets/MSetGenTree.v')
| -rw-r--r-- | theories/MSets/MSetGenTree.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 3142d97ca..6164e6e93 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -962,7 +962,8 @@ Proof. firstorder. Qed. Lemma eq_Leq : forall s s', eq s s' <-> L.eq (elements s) (elements s'). Proof. unfold eq, Equal, L.eq; intros. - setoid_rewrite elements_spec1; firstorder. + do 2 setoid_rewrite elements_spec1. (*FIXME due to regression in rewrite *) + firstorder. Qed. Definition lt (s1 s2 : tree) : Prop := |