X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fpts_dummy_new%2Fterms.ma;h=1291013ffd79807624d9ee4fb85db946f3e54a21;hb=7c9d99dfb049d726491b71f07ba6a9b088b30166;hp=0227f1e948e3787f6269b58c252f5558b427ad8d;hpb=46e87acb755894f9234191d675eeb5db4f5b930b;p=helm.git diff --git a/matita/matita/lib/pts_dummy_new/terms.ma b/matita/matita/lib/pts_dummy_new/terms.ma index 0227f1e94..1291013ff 100644 --- a/matita/matita/lib/pts_dummy_new/terms.ma +++ b/matita/matita/lib/pts_dummy_new/terms.ma @@ -9,8 +9,8 @@ \ / V_______________________________________________________________ *) -include "basics/list.ma". -include "lambda/lambda_notation.ma". +include "basics/lists/list.ma". +include "pts_dummy/lambda_notation.ma". inductive T : Type[0] ≝ | Sort: nat → T (* starts from 0 *)