fully qualify all library names

DanGrayson · DanGrayson · commit 73b0b9c8375c · 2013-11-02T14:42:56.000-04:00
diff --git a/Generalities/uu0.v b/Generalities/uu0.v
@@ -16,7 +16,7 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
 
 (** Imports *)
 
-Require Export uuu.
+Require Export Foundations.Generalities.uuu.
 
 (** Universe structure *)
 
diff --git a/Proof_of_Extensionality/funextfun.v b/Proof_of_Extensionality/funextfun.v
@@ -11,7 +11,7 @@ This file contains the formulation of the univalence axiom and the proof that it
 
 Unset Automatic Introduction. (** This line has to be removed for the file to compile with Coq8.2 *)
 
-Require Export uu0.
+Require Export Foundations.Generalities.uu0.
 
 
 (** ** Univalence axiom. *)
diff --git a/hlevel1/hProp.v b/hlevel1/hProp.v
@@ -26,7 +26,7 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
 (** Imports *)
 
 
-Require Export uu0 . 
+Require Export Foundations.Generalities.uu0 . 
 
 (** Universe structure *)
 
diff --git a/hlevel2/algebra1a.v b/hlevel2/algebra1a.v
@@ -13,7 +13,7 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 
 (** Imports *)
 
-Require Export hSet .
+Require Export Foundations.hlevel2.hSet .
 
 
 (** To upstream files *)
diff --git a/hlevel2/algebra1b.v b/hlevel2/algebra1b.v
@@ -13,7 +13,7 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 
 (** Imports *)
 
-Require Export algebra1a .
+Require Export Foundations.hlevel2.algebra1a .
 
 
 (** To upstream files *)
diff --git a/hlevel2/algebra1c.v b/hlevel2/algebra1c.v
@@ -13,7 +13,7 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 
 (** Imports *)
 
-Require Export algebra1b .
+Require Export Foundations.hlevel2.algebra1b .
 
 
 (** To upstream files *)
diff --git a/hlevel2/algebra1d.v b/hlevel2/algebra1d.v
@@ -13,7 +13,7 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 
 (** Imports *)
 
-Require Export algebra1c .
+Require Export Foundations.hlevel2.algebra1c .
 
 
 (** To upstream files *)
diff --git a/hlevel2/finitesets.v b/hlevel2/finitesets.v
@@ -18,9 +18,9 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
 
 (** Imports. *)
 
-Require Export hProp .
-Require Export stnfsets .
-Require Export hSet .  
+Require Export Foundations.hlevel1.hProp .
+Require Export Foundations.hlevel2.stnfsets .
+Require Export Foundations.hlevel2.hSet .  
 
 
 
diff --git a/hlevel2/hSet.v b/hlevel2/hSet.v
@@ -17,7 +17,7 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 
 (** Imports *)
 
-Require Export hProp .
+Require Export Foundations.hlevel1.hProp .
 
 
 (** ** The type of sets i.e. of types of h-level 2 in [ UU ] *) 
diff --git a/hlevel2/hnat.v b/hlevel2/hnat.v
@@ -17,7 +17,7 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
 
 (** Imports. *)
 
-Require Export algebra1d . 
+Require Export Foundations.hlevel2.algebra1d . 
 
 (** To up-stream files  *)
 
diff --git a/hlevel2/hq.v b/hlevel2/hq.v
@@ -16,7 +16,7 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 
 (** Imports *)
 
-Require Export hz .
+Require Export Foundations.hlevel2.hz .
 
 Opaque hz . 
 
diff --git a/hlevel2/hz.v b/hlevel2/hz.v
@@ -16,8 +16,8 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 
 (** Imports *)
 
-Require Export hnat .
-Require Export algebra1d .
+Require Export Foundations.hlevel2.hnat .
+Require Export Foundations.hlevel2.algebra1d .
 
 
 (** Upstream *)
diff --git a/hlevel2/stnfsets.v b/hlevel2/stnfsets.v
@@ -16,10 +16,10 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
 (** Imports. *)
 
 
-Require Export hnat .
+Require Export Foundations.hlevel2.hnat .
 
 
-(* To up-steram files *)
+(* To up-stream files *)
 
 
 
