X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Flogic%2Fequality.ma;h=77ef0eb82ca2064213d49b0106cf82994a8917e0;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=87fe22bac85c4a9e592b8f38735c3f9e857c67ca;hpb=3eff4cc36820df9faddb3cb16390717851db499c;p=helm.git

diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index 87fe22bac..77ef0eb82 100644
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -19,8 +19,10 @@ include "higher_order_defs/relations.ma".
 inductive eq (A:Type) (x:A) : A \to Prop \def
     refl_eq : eq A x x.
 
+(*CSC: the URI must disappear: there is a bug now *)
 interpretation "leibnitz's equality"
    'eq x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y).
+(*CSC: this alias should disappear. It is now required because the notation for Coq is pre-loaded *)
 alias symbol "eq" (instance 0) = "leibnitz's equality".