fixed typo in 'leq interpretation uri which enable nice rendering of

[helm.git] / helm / matita / core_notation.ma

diff --git a/helm/matita/core_notation.ma b/helm/matita/core_notation.ma
index 88cd759b806390d96c172d9be7e59f5fd84a8029..486e921b5d4ba717bb317976e8ec8736c48def1d 100644 (file)
--- 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).