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

diff --git a/matita/matita/lib/hott/Overture.ma b/matita/matita/lib/hott/Overture.ma
index 3725123cc..e02683ffa 100644
--- a/matita/matita/lib/hott/Overture.ma
+++ b/matita/matita/lib/hott/Overture.ma
@@ -1,4 +1,5 @@
 include "hott/types.ma".
+include "basics/core_notation/compose_2.ma".
 
 (* * * Basic definitions of homotopy type theory, particularly the groupoid structure of identity types. *)