X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fhott%2Fpts.ma;h=cf788829272ed59b79505aea66ea6bc8efa6ead5;hb=bfc9b5c983a046e1fcd111dbe8518c827643861e;hp=1e6dfca136cf55337c2c404d3f6c1d655507747e;hpb=9cfd213efc96e1bd60207d4edbf8c21ca80b6d80;p=helm.git diff --git a/matita/matita/lib/hott/pts.ma b/matita/matita/lib/hott/pts.ma index 1e6dfca13..cf7888292 100644 --- a/matita/matita/lib/hott/pts.ma +++ b/matita/matita/lib/hott/pts.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "notations.ma". +include "hott/notations.ma". universe constraint Type[0] < Type[1]. universe constraint Type[1] < Type[2].