add loadpath commands for interactive "Foundations" access

DanGrayson · DanGrayson · commit aadd0e80875f · 2013-11-02T17:18:22.000-04:00
Now that we are using fully qualified library names, such as
Foundations.Generalities.uu0, we have to arrange for coqtop to work, especially
when run by Proof General.  One way would be to give it "-R . Foundations" as
command line options.  But Proof General has a strange sort of bug that causes
it to loop forever when starting up coq after you evaluate

     (setq coq-prog-args '("-emacs" "-R" "." "Foo"))

.  The best solution seems to be to add lines

      Add LoadPath ".." as Foundations.

to our *.v source files, which we do in this commit.
diff --git a/Generalities/uu0.v b/Generalities/uu0.v
@@ -16,6 +16,8 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
 
 (** Imports *)
 
+Add LoadPath ".." as Foundations.
+
 Require Export Foundations.Generalities.uuu.
 
 (** Universe structure *)
diff --git a/Proof_of_Extensionality/funextfun.v b/Proof_of_Extensionality/funextfun.v
@@ -11,6 +11,8 @@ 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 *)
 
+Add LoadPath ".." as Foundations.
+
 Require Export Foundations.Generalities.uu0.
 
 
diff --git a/hlevel1/hProp.v b/hlevel1/hProp.v
@@ -25,6 +25,7 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
 
 (** Imports *)
 
+Add LoadPath ".." as Foundations.
 
 Require Export Foundations.Generalities.uu0 . 
 
diff --git a/hlevel2/algebra1a.v b/hlevel2/algebra1a.v
@@ -13,6 +13,8 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 
 (** Imports *)
 
+Add LoadPath ".." as Foundations.
+
 Require Export Foundations.hlevel2.hSet .
 
 
diff --git a/hlevel2/algebra1b.v b/hlevel2/algebra1b.v
@@ -13,6 +13,8 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 
 (** Imports *)
 
+Add LoadPath ".." as Foundations.
+
 Require Export Foundations.hlevel2.algebra1a .
 
 
diff --git a/hlevel2/algebra1c.v b/hlevel2/algebra1c.v
@@ -13,6 +13,8 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 
 (** Imports *)
 
+Add LoadPath ".." as Foundations.
+
 Require Export Foundations.hlevel2.algebra1b .
 
 
diff --git a/hlevel2/algebra1d.v b/hlevel2/algebra1d.v
@@ -13,6 +13,8 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 
 (** Imports *)
 
+Add LoadPath ".." as Foundations.
+
 Require Export Foundations.hlevel2.algebra1c .
 
 
diff --git a/hlevel2/finitesets.v b/hlevel2/finitesets.v
@@ -18,6 +18,8 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
 
 (** Imports. *)
 
+Add LoadPath ".." as Foundations.
+
 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,6 +17,8 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 
 (** Imports *)
 
+Add LoadPath ".." as Foundations.
+
 Require Export Foundations.hlevel1.hProp .
 
 
diff --git a/hlevel2/hnat.v b/hlevel2/hnat.v
@@ -17,6 +17,8 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
 
 (** Imports. *)
 
+Add LoadPath ".." as Foundations.
+
 Require Export Foundations.hlevel2.algebra1d . 
 
 (** To up-stream files  *)
diff --git a/hlevel2/hq.v b/hlevel2/hq.v
@@ -16,6 +16,8 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 
 (** Imports *)
 
+Add LoadPath ".." as Foundations.
+
 Require Export Foundations.hlevel2.hz .
 
 Opaque hz . 
diff --git a/hlevel2/hz.v b/hlevel2/hz.v
@@ -16,6 +16,8 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
 
 (** Imports *)
 
+Add LoadPath ".." as Foundations.
+
 Require Export Foundations.hlevel2.hnat .
 Require Export Foundations.hlevel2.algebra1d .
 
diff --git a/hlevel2/stnfsets.v b/hlevel2/stnfsets.v
@@ -15,6 +15,7 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
 
 (** Imports. *)
 
+Add LoadPath ".." as Foundations.
 
 Require Export Foundations.hlevel2.hnat .
 

Original file line number	Diff line number	Diff line change
`@@ -25,6 +25,7 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com`
`25`	`25`
`26`	`26`	`(** Imports *)`
`27`	`27`
	`28`	`+Add LoadPath ".." as Foundations.`
`28`	`29`
`29`	`30`	`Require Export Foundations.Generalities.uu0 .`
`30`	`31`
Original file line number	Diff line number	Diff line change
`@@ -15,6 +15,7 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com`
`15`	`15`
`16`	`16`	`(** Imports. *)`
`17`	`17`
	`18`	`+Add LoadPath ".." as Foundations.`
`18`	`19`
`19`	`20`	`Require Export Foundations.hlevel2.hnat .`
`20`	`21`