diff options
Diffstat (limited to 'theories/MSets')
| -rw-r--r-- | theories/MSets/MSetPositive.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v index a15b533d3d..4f2f4256e2 100644 --- a/theories/MSets/MSetPositive.v +++ b/theories/MSets/MSetPositive.v @@ -771,7 +771,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Proof. unfold Exists, In. intro f. induction s as [|l IHl o r IHr]; intros i; simpl. - firstorder. + firstorder with bool. rewrite <- 2orb_lazy_alt, 2orb_true_iff, <- andb_lazy_alt, andb_true_iff. rewrite IHl, IHr. clear IHl IHr. split. |