From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 4 Mar 2014 16:07:36 +0000 (+0000)
Subject: Inclusions improved to allow compilation from the toplevel.
X-Git-Tag: make_still_working~959
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=bfc9b5c983a046e1fcd111dbe8518c827643861e

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 0c886056d..3725123cc 100644
--- 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 1e6dfca13..cf7888292 100644
--- 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 4db2b76ef..9378c184d 100644
--- 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;