Skip to content

Commit 42d0d39

Browse files
DanGraysonDanGrayson
committed
comment out the recently added lines Add LoadPath ".." as Foundations
The reason is that the path is relative, but not relative to the directory containing the source file, but rather, relative to the current working directory of the compiler. This can cause confusion if a sibling to the top level directory of this repository happens to be called "Foundations", because coq_makefile generates compilation commands that are run in the top level directory.
1 parent aadd0e8 commit 42d0d39

File tree

13 files changed

+13
-13
lines changed

13 files changed

+13
-13
lines changed

‎Generalities/uu0.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
1616

1717
(** Imports *)
1818

19-
Add LoadPath ".." as Foundations.
19+
(* Add LoadPath ".." as Foundations. *)
2020

2121
Require Export Foundations.Generalities.uuu.
2222

‎Proof_of_Extensionality/funextfun.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ This file contains the formulation of the univalence axiom and the proof that it
1111

1212
Unset Automatic Introduction. (** This line has to be removed for the file to compile with Coq8.2 *)
1313

14-
Add LoadPath ".." as Foundations.
14+
(* Add LoadPath ".." as Foundations. *)
1515

1616
Require Export Foundations.Generalities.uu0.
1717

‎hlevel1/hProp.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
2525

2626
(** Imports *)
2727

28-
Add LoadPath ".." as Foundations.
28+
(* Add LoadPath ".." as Foundations. *)
2929

3030
Require Export Foundations.Generalities.uu0 .
3131

‎hlevel2/algebra1a.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
1313

1414
(** Imports *)
1515

16-
Add LoadPath ".." as Foundations.
16+
(* Add LoadPath ".." as Foundations. *)
1717

1818
Require Export Foundations.hlevel2.hSet .
1919

‎hlevel2/algebra1b.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
1313

1414
(** Imports *)
1515

16-
Add LoadPath ".." as Foundations.
16+
(* Add LoadPath ".." as Foundations. *)
1717

1818
Require Export Foundations.hlevel2.algebra1a .
1919

‎hlevel2/algebra1c.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
1313

1414
(** Imports *)
1515

16-
Add LoadPath ".." as Foundations.
16+
(* Add LoadPath ".." as Foundations. *)
1717

1818
Require Export Foundations.hlevel2.algebra1b .
1919

‎hlevel2/algebra1d.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
1313

1414
(** Imports *)
1515

16-
Add LoadPath ".." as Foundations.
16+
(* Add LoadPath ".." as Foundations. *)
1717

1818
Require Export Foundations.hlevel2.algebra1c .
1919

‎hlevel2/finitesets.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
1818

1919
(** Imports. *)
2020

21-
Add LoadPath ".." as Foundations.
21+
(* Add LoadPath ".." as Foundations. *)
2222

2323
Require Export Foundations.hlevel1.hProp .
2424
Require Export Foundations.hlevel2.stnfsets .

‎hlevel2/hSet.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
1717

1818
(** Imports *)
1919

20-
Add LoadPath ".." as Foundations.
20+
(* Add LoadPath ".." as Foundations. *)
2121

2222
Require Export Foundations.hlevel1.hProp .
2323

‎hlevel2/hnat.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
1717

1818
(** Imports. *)
1919

20-
Add LoadPath ".." as Foundations.
20+
(* Add LoadPath ".." as Foundations. *)
2121

2222
Require Export Foundations.hlevel2.algebra1d .
2323

‎hlevel2/hq.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
1616

1717
(** Imports *)
1818

19-
Add LoadPath ".." as Foundations.
19+
(* Add LoadPath ".." as Foundations. *)
2020

2121
Require Export Foundations.hlevel2.hz .
2222

‎hlevel2/hz.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
1616

1717
(** Imports *)
1818

19-
Add LoadPath ".." as Foundations.
19+
(* Add LoadPath ".." as Foundations. *)
2020

2121
Require Export Foundations.hlevel2.hnat .
2222
Require Export Foundations.hlevel2.algebra1d .

‎hlevel2/stnfsets.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
1515

1616
(** Imports. *)
1717

18-
Add LoadPath ".." as Foundations.
18+
(* Add LoadPath ".." as Foundations. *)
1919

2020
Require Export Foundations.hlevel2.hnat .
2121

0 commit comments

Comments
 (0)