diff options
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FMapFacts.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FSetFacts.v | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 6d77a6a0cc..617ea6f4f6 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -651,7 +651,7 @@ Proof. unfold Equal; congruence. Qed. Definition Equal_ST : forall elt:Type, Setoid_Theory (t elt) (@Equal _). Proof. -constructor; [apply Equal_refl | apply Equal_sym | apply Equal_trans]. +constructor; red; [apply Equal_refl | apply Equal_sym | apply Equal_trans]. Qed. Add Relation key E.eq diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index 0c19176f82..6afb8fcb7b 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 |