aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets')
-rw-r--r--theories/FSets/FSetBridge.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index d267991c3c..73021a84a3 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -772,7 +772,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
generalize C; unfold compat_bool, Proper, respectful; intros; apply (f_equal negb);
auto.
simpl; unfold Equal; intuition.
- apply filter_3; firstorder.
+ apply filter_3; firstorder with bool.
elim (H2 a); intros.
assert (In a s).
eapply filter_1; eauto.