X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fhott%2FOverture.ma;fp=matita%2Fmatita%2Flib%2Fhott%2FOverture.ma;h=3725123cce1e23424349e2f6dd848c6095668663;hb=bfc9b5c983a046e1fcd111dbe8518c827643861e;hp=0c886056dd4a1dcbe878b3d6f9b43c03411c9698;hpb=9cfd213efc96e1bd60207d4edbf8c21ca80b6d80;p=helm.git

diff --git a/matita/matita/lib/hott/Overture.ma b/matita/matita/lib/hott/Overture.ma
index 0c886056d..3725123cc 100644
--- a/matita/matita/lib/hott/Overture.ma
+++ b/matita/matita/lib/hott/Overture.ma
@@ -1,4 +1,4 @@
-include "types.ma".
+include "hott/types.ma".
 
 (* * * Basic definitions of homotopy type theory, particularly the groupoid structure of identity types. *)
 
@@ -444,4 +444,4 @@ Ltac atomic x :=
     | forall _, _ => fail 1 x "is not atomic"
     | _ => idtac
   end.
-*)
\ No newline at end of file
+*)