Keeping track of locations of disambiguated ids and symbols.

[helm.git] / matitaB / matita / nlibrary / properties / relations.ma

diff --git a/matitaB/matita/nlibrary/properties/relations.ma b/matitaB/matita/nlibrary/properties/relations.ma
index 1df2e205a5d097a2680ad0864d92145ada7c9906..334c67842f8762ecee087a7dd103f8ba0e886345 100644 (file)
--- a/matitaB/matita/nlibrary/properties/relations.ma
+++ b/matitaB/matita/nlibrary/properties/relations.ma
@@ -20,7 +20,7 @@ definition transitive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀z,x,y. P x z
 
 record equivalence_relation (A:Type[0]) : Type[1] ≝
  { eq_rel:2> A → A → CProp[0];
-   refl: reflexive ? eq_rel;
-   sym: symmetric ? eq_rel;
-   trans: transitive ? eq_rel
+   refl: <A href="cic:/matita/ng/properties/relations/reflexive.def(1)">reflexive</A> ? eq_rel;
+   sym: <A href="cic:/matita/ng/properties/relations/symmetric.def(1)">symmetric</A> ? eq_rel;
+   trans: <A href="cic:/matita/ng/properties/relations/transitive.def(1)">transitive</A> ? eq_rel
  }.