decentralizing core notation

[helm.git] / matita / matita / lib / hott / Overture.ma

diff --git a/matita/matita/lib/hott/Overture.ma b/matita/matita/lib/hott/Overture.ma
index 3725123cce1e23424349e2f6dd848c6095668663..e02683ffa8650caad5010be9e2904dea502f0c6d 100644 (file)
--- 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. *)