diff options
Diffstat (limited to 'theories/FSets/FSetFacts.v')
| -rw-r--r-- | theories/FSets/FSetFacts.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index 0c19176f8..6afb8fcb7 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -295,12 +295,12 @@ End BoolSpec. Definition E_ST : Setoid_Theory elt E.eq. Proof. -constructor; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans]. +constructor ; red; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans]. Qed. Definition Equal_ST : Setoid_Theory t Equal. Proof. -constructor; [apply eq_refl | apply eq_sym | apply eq_trans]. +constructor ; red; [apply eq_refl | apply eq_sym | apply eq_trans]. Qed. Add Relation elt E.eq |