Inclusions improved to allow compilation from the toplevel.

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

diff --git a/matita/matita/lib/hott/pts.ma b/matita/matita/lib/hott/pts.ma
index 1e6dfca136cf55337c2c404d3f6c1d655507747e..cf788829272ed59b79505aea66ea6bc8efa6ead5 100644 (file)
--- a/matita/matita/lib/hott/pts.ma
+++ b/matita/matita/lib/hott/pts.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "notations.ma".
+include "hott/notations.ma".
 
 universe constraint Type[0] < Type[1].
 universe constraint Type[1] < Type[2].

diff --git a/matita/matita/lib/hott/types.ma b/matita/matita/lib/hott/types.ma
index 4db2b76ef01d3ba6c5789d224aa9ce326d3dfa20..9378c184de6d534de25f1dda5baa9b567c982a03 100644 (file)
--- a/matita/matita/lib/hott/types.ma
+++ b/matita/matita/lib/hott/types.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "pts.ma".
+include "hott/pts.ma".
 
 record Exists (A: Type[0]) (P: A → Type[0]) : Type[0] ≝ {
  pr1: A;