aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThéo Zimmermann2019-12-16 15:51:56 +0100
committerThéo Zimmermann2019-12-16 15:51:56 +0100
commita9ed928ac9cf245b802c93f7952888817bc2e50c (patch)
tree78d612bd0d23e1de73dc1daf5c9dcff9a84c820d
parent1df9e71a1f9b0729a17d09e009add2e87fcde5ad (diff)
parent7a9df17e8520fe1b7dc6a236ef320469a8964c9f (diff)
Merge PR #11291: Being explicit on existence of a remote link in stdlib to avoid possible "breach of privacy"
Reviewed-by: Zimmi48
-rw-r--r--theories/Logic/Hurkens.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 9aed952183..d9e89d6b91 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -72,7 +72,7 @@
- [[Geuvers01]] H. Geuvers, "Inconsistency of Classical Logic in Type
Theory", 2001, revised 2007
- (see {{http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz}}).
+ (see external link {{http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz}}).
*)