]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/lib/hott/Overture.ma
decentralizing core notation
[helm.git] / matita / matita / lib / hott / Overture.ma
index 0c886056dd4a1dcbe878b3d6f9b43c03411c9698..e02683ffa8650caad5010be9e2904dea502f0c6d 100644 (file)
@@ -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
+*)