X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fnlibrary%2Flogic%2Fpts.ma;h=1fed8525640c26c3616c67063f1085c491f7c95e;hb=d7a1ab434c222c2445f36b7a3b6234d1f57f9794;hp=d9db8c39f553b40e581296e7e27e48bf0ac9c7dd;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/matita/nlibrary/logic/pts.ma b/matita/matita/nlibrary/logic/pts.ma
index d9db8c39f..1fed85256 100644
--- a/matita/matita/nlibrary/logic/pts.ma
+++ b/matita/matita/nlibrary/logic/pts.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "core_notation.ma".
+
 universe constraint Type[0] < Type[1].
 universe constraint Type[1] < Type[2].
 universe constraint Type[2] < Type[3].