removed work-arounds for poor disambiguation, which should now be fixed with the...

[helm.git] / helm / matita / library / logic / equality.ma

diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index 87fe22bac85c4a9e592b8f38735c3f9e857c67ca..a561827f8a83e1db22e18af1d836c10d572f3509 100644 (file)
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -19,11 +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).
-alias symbol "eq" (instance 0) = "leibnitz's equality".
 
-    
 theorem reflexive_eq : \forall A:Type. reflexive A (eq A).
 simplify.intros.apply refl_eq.
 qed.