Error when [foo.(bar)] is used with nonprojection [bar]

(warn if bar is a nonprimitive projection)

1 files changed, 3 insertions, 3 deletions

diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index 346c300ee5..4591c7ed94 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -128,9 +128,9 @@ Module Type DecidableTypeFull' := DecidableTypeFull <+ EqNotation.
       [EqualityType] and [DecidableType] *)
 
 Module BackportEq (E:Eq)(F:IsEq E) <: IsEqOrig E.
- Definition eq_refl := F.eq_equiv.(@Equivalence_Reflexive _ _). 
- Definition eq_sym := F.eq_equiv.(@Equivalence_Symmetric _ _).
- Definition eq_trans := F.eq_equiv.(@Equivalence_Transitive _ _).
+ Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv.
+ Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv.
+ Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv.
 End BackportEq.
 
 Module UpdateEq (E:Eq)(F:IsEqOrig E) <: IsEq E.