From 3fdb62dee9830bb551798ee9c3dd2a3af1493e8d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 26 Oct 2018 16:55:54 +0200
Subject: Error when [foo.(bar)] is used with nonprojection [bar]

(warn if bar is a nonprimitive projection)
---
 theories/Structures/Equalities.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'theories/Structures')

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.
-- 
cgit v1.2.3