Inclusions improved to allow compilation from the toplevel.

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

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;