X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fexcedence.ma;h=fa6848e120314b987eaa0f61bf81cec57d42dea6;hb=c0f86a886451a0df3b42a1435e21b5def9f34792;hp=1bddcb16eabdc9876b0c3219650de8a176485b3d;hpb=feaabb3c45906fafb4b6eb3fb10add6e6da6069b;p=helm.git

diff --git a/helm/software/matita/dama/excedence.ma b/helm/software/matita/dama/excedence.ma
index 1bddcb16e..fa6848e12 100644
--- a/helm/software/matita/dama/excedence.ma
+++ b/helm/software/matita/dama/excedence.ma
@@ -52,7 +52,7 @@ record apartness : Type ≝ {
 }.
 
 notation "a break # b" non associative with precedence 50 for @{ 'apart $a $b}.
-interpretation "axiomatic apartness" 'apart x y = 
+interpretation "apartness" 'apart x y = 
   (cic:/matita/excedence/ap_apart.con _ x y).
 
 definition strong_ext ≝ λA:apartness.λop:A→A.∀x,y. op x # op y → x # y.