A few changes to factorization and gcd.

[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 77ef0eb82ca2064213d49b0106cf82994a8917e0..a5d2f0d1e461cd5c02e95aa5f2eb1ec04f96d5fd 100644 (file)
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -22,10 +22,11 @@ inductive eq (A:Type) (x:A) : A \to Prop \def
 (*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".
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "leibnitz's non-equality"
+  'neq x y = (cic:/matita/logic/connectives/Not.con
+    (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y)).
 
-    
 theorem reflexive_eq : \forall A:Type. reflexive A (eq A).
 simplify.intros.apply refl_eq.
 qed.