X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fcore_notation.ma;h=486e921b5d4ba717bb317976e8ec8736c48def1d;hb=dc861d214cb992a898f81752614201b8074eef12;hp=88cd759b806390d96c172d9be7e59f5fd84a8029;hpb=6b5e1d495c61f459738187e8d71efadb162abdbe;p=helm.git

diff --git a/helm/matita/core_notation.ma b/helm/matita/core_notation.ma
index 88cd759b8..486e921b5 100644
--- a/helm/matita/core_notation.ma
+++ b/helm/matita/core_notation.ma
@@ -93,7 +93,7 @@ interpretation "binary integer unary minus" 'uminus x = (cic:/Coq/ZArith/BinInt/
 
 (* relational operators *)
 
-interpretation "natural 'less or equal to'" 'leq x y = (cic:/Coq/Init/Peano/le.ind x y).
+interpretation "natural 'less or equal to'" 'leq x y = (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y).
 interpretation "real 'less or equal to'" 'leq x y = (cic:/Coq/Reals/Rdefinitions/Rle.con x y).
 interpretation "natural 'greater or equal to'" 'geq x y = (cic:/Coq/Init/Peano/ge.con x y).
 interpretation "real 'greater or equal to'" 'geq x y = (cic:/Coq/Reals/Rdefinitions/Rge.con x y).