- new component for restricted computation (delta, zeta and tau only)

[helm.git] / matita / matita / nlibrary / logic / pts.ma

diff --git a/matita/matita/nlibrary/logic/pts.ma b/matita/matita/nlibrary/logic/pts.ma
index d9db8c39f553b40e581296e7e27e48bf0ac9c7dd..1fed8525640c26c3616c67063f1085c491f7c95e 100644 (file)
--- 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].