Changed Makefile such that RezkCompletion compiles as before.

vladimirias · vladimirias · commit 6c7aa562bb88 · 2014-01-03T17:06:33.000-05:00
diff --git a/Makefile b/Makefile
@@ -1,39 +1,39 @@
 all : hlevel2/hq.vo hlevel2/finitesets.vo  Proof_of_Extensionality/funextfun.vo
 
 hlevel2/hq.vo : hlevel2/hq.v hlevel2/hz.vo
-	cd hlevel2/ && coqc hq
+	cd hlevel2/ && coqc -R . Foundations.hlevel2 hq
 hlevel2/hz.vo : hlevel2/hz.v hlevel2/hnat.vo
-	cd hlevel2/ && coqc hz
+	cd hlevel2/ && coqc -R . Foundations.hlevel2 hz
 
 hlevel2/finitesets.vo : hlevel2/finitesets.v hlevel2/stnfsets.vo
-	cd hlevel2/ && coqc finitesets
+	cd hlevel2/ && coqc -R . Foundations.hlevel2 finitesets
 hlevel2/stnfsets.vo : hlevel2/stnfsets.v hlevel2/hnat.vo
-	cd hlevel2/ && coqc stnfsets
+	cd hlevel2/ && coqc -R . Foundations.hlevel2 stnfsets
 
 hlevel2/hnat.vo : hlevel2/hnat.v hlevel2/algebra1d.vo
-	cd hlevel2/ && coqc hnat
+	cd hlevel2/ && coqc -R . Foundations.hlevel2 hnat
 hlevel2/algebra1d.vo : hlevel2/algebra1d.v hlevel2/algebra1c.vo
-	cd hlevel2/ && coqc algebra1d
+	cd hlevel2/ && coqc -R . Foundations.hlevel2 algebra1d
 hlevel2/algebra1c.vo : hlevel2/algebra1c.v hlevel2/algebra1b.vo
-	cd hlevel2/ && coqc algebra1c
+	cd hlevel2/ && coqc -R . Foundations.hlevel2 algebra1c
 hlevel2/algebra1b.vo : hlevel2/algebra1b.v hlevel2/algebra1a.vo
-	cd hlevel2/ && coqc algebra1b
+	cd hlevel2/ && coqc -R . Foundations.hlevel2 algebra1b
 hlevel2/algebra1a.vo : hlevel2/algebra1a.v hlevel2/hSet.vo
-	cd hlevel2/ && coqc algebra1a
+	cd hlevel2/ && coqc -R . Foundations.hlevel2 algebra1a
 
 hlevel2/hSet.vo : hlevel2/hSet.v hlevel1/hProp.vo
-	cd hlevel2/ && coqc hSet
+	cd hlevel2/ && coqc -R . Foundations.hlevel2 hSet
 
 hlevel1/hProp.vo : hlevel1/hProp.v Generalities/uu0.vo
-	cd hlevel1/ && coqc hProp
+	cd hlevel1/ && coqc -R . Foundations.hlevel1 hProp
 
 Proof_of_Extensionality/funextfun.vo : Proof_of_Extensionality/funextfun.v Generalities/uu0.vo
-	cd Proof_of_Extensionality/ && coqc funextfun
+	cd Proof_of_Extensionality/ && coqc -R . Foundations.Proof_of_Extensionality funextfun
 
 Generalities/uu0.vo : Generalities/uu0.v Generalities/uuu.vo
-	cd Generalities/ && coqc uu0
+	cd Generalities/ && coqc -R . Foundations.Generalities uu0
 Generalities/uuu.vo : Generalities/uuu.v
-	cd Generalities/ && coqc uuu
+	cd Generalities/ && coqc -R . Foundations.Generalities uuu
 
 
 clean : 
diff --git a/Proof_of_Extensionality/funextfun.v b/Proof_of_Extensionality/funextfun.v
@@ -13,6 +13,7 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 
 Add LoadPath "../Generalities".
 
+Require Export "uuu".
 Require Export "uu0".
 
 
diff --git a/hlevel1/hProp.v b/hlevel1/hProp.v
@@ -27,6 +27,7 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
 
 Add LoadPath "../Generalities" .
 
+Require Export "uuu".
 Require Export "uu0" . 
 
 (** Universe structure *)
diff --git a/hlevel2/algebra1a.v b/hlevel2/algebra1a.v
@@ -16,7 +16,10 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 Add LoadPath "../hlevel1" .
 Add LoadPath "../Generalities".
 
-Require Export hSet .
+Require Export "uuu".
+Require Export "uu0" . 
+Require Export "hProp" .
+Require Export "hSet" .
 
 
 (** To upstream files *)
diff --git a/hlevel2/algebra1b.v b/hlevel2/algebra1b.v
@@ -16,7 +16,11 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 Add LoadPath "../hlevel1" .
 Add LoadPath "../Generalities".
 
-Require Export algebra1a .
+Require Export "uuu".
+Require Export "uu0" . 
+Require Export "hProp" .
+Require Export "hSet" .
+Require Export "algebra1a" .
 
 
 (** To upstream files *)
diff --git a/hlevel2/algebra1c.v b/hlevel2/algebra1c.v
@@ -16,7 +16,12 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 Add LoadPath "../hlevel1" .
 Add LoadPath "../Generalities".
 
-Require Export algebra1b .
+Require Export "uuu".
+Require Export "uu0" . 
+Require Export "hProp" .
+Require Export "hSet" .
+Require Export "algebra1a" .
+Require Export "algebra1b" .
 
 
 (** To upstream files *)
diff --git a/hlevel2/algebra1d.v b/hlevel2/algebra1d.v
@@ -16,7 +16,13 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 Add LoadPath "../hlevel1" .
 Add LoadPath "../Generalities".
 
-Require Export algebra1c .
+Require Export "uuu".
+Require Export "uu0" . 
+Require Export "hProp" .
+Require Export "hSet" .
+Require Export "algebra1a" .
+Require Export "algebra1b" .
+Require Export "algebra1c" .
 
 
 (** To upstream files *)
diff --git a/hlevel2/finitesets.v b/hlevel2/finitesets.v
@@ -21,7 +21,16 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
 Add LoadPath "../hlevel1" .
 Add LoadPath "../Generalities".
 
-Require Export stnfsets .
+Require Export "uuu".
+Require Export "uu0" . 
+Require Export "hProp" .
+Require Export "hSet" .
+Require Export "algebra1a" .
+Require Export "algebra1b" .
+Require Export "algebra1c" .
+Require Export "algebra1d" . 
+Require Export "hnat" .
+Require Export "stnfsets" .
 
 
 
diff --git a/hlevel2/hSet.v b/hlevel2/hSet.v
@@ -20,7 +20,10 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 Add LoadPath "../hlevel1" .
 Add LoadPath "../Generalities".
 
-Require Export hProp .
+
+Require Export "uuu".
+Require Export "uu0" . 
+Require Export "hProp" .
 
 
 
diff --git a/hlevel2/hnat.v b/hlevel2/hnat.v
@@ -20,7 +20,14 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
 Add LoadPath "../hlevel1" .
 Add LoadPath "../Generalities".
 
-Require Export algebra1d . 
+Require Export "uuu".
+Require Export "uu0" . 
+Require Export "hProp" .
+Require Export "hSet" .
+Require Export "algebra1a" .
+Require Export "algebra1b" .
+Require Export "algebra1c" .
+Require Export "algebra1d" . 
 
 (** To up-stream files  *)
 
diff --git a/hlevel2/hq.v b/hlevel2/hq.v
@@ -19,7 +19,16 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 Add LoadPath "../hlevel1" .
 Add LoadPath "../Generalities".
 
-Require Export hz .
+Require Export "uuu".
+Require Export "uu0" . 
+Require Export "hProp" .
+Require Export "hSet" .
+Require Export "algebra1a" .
+Require Export "algebra1b" .
+Require Export "algebra1c" .
+Require Export "algebra1d" . 
+Require Export "hnat" .
+Require Export "hz" .
 
 Opaque hz . 
 
diff --git a/hlevel2/hz.v b/hlevel2/hz.v
@@ -19,7 +19,15 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 Add LoadPath "../hlevel1" .
 Add LoadPath "../Generalities".
 
-Require Export hnat .
+Require Export "uuu".
+Require Export "uu0" . 
+Require Export "hProp" .
+Require Export "hSet" .
+Require Export "algebra1a" .
+Require Export "algebra1b" .
+Require Export "algebra1c" .
+Require Export "algebra1d" . 
+Require Export "hnat" .
 
 
 
diff --git a/hlevel2/stnfsets.v b/hlevel2/stnfsets.v
@@ -18,7 +18,15 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
 Add LoadPath "../hlevel1" .
 Add LoadPath "../Generalities".
 
-Require Export hnat .
+Require Export "uuu".
+Require Export "uu0" . 
+Require Export "hProp" .
+Require Export "hSet" .
+Require Export "algebra1a" .
+Require Export "algebra1b" .
+Require Export "algebra1c" .
+Require Export "algebra1d" . 
+Require Export "hnat" .
 
 
 (* To up-stream files *)

Original file line number	Diff line number	Diff line change
`@@ -13,6 +13,7 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co`
`13`	`13`
`14`	`14`	`Add LoadPath "../Generalities".`
`15`	`15`
	`16`	`+Require Export "uuu".`
`16`	`17`	`Require Export "uu0".`
`17`	`18`
`18`	`19`