X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fhott%2FOverture.ma;h=e02683ffa8650caad5010be9e2904dea502f0c6d;hb=aad5588b82d0f2991c336f7ac2f3fadd76768eeb;hp=0c886056dd4a1dcbe878b3d6f9b43c03411c9698;hpb=90dd88139a78b4dd650d5c462ecf602bf4813cd4;p=helm.git

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