aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Paul Steckler <steck@stecksoft.com>2016-08-22 15:31:24 -0400
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-08-23 14:12:53 +0200
commit50bece7c25e62132bc06c3bb0261937c657319d3 (patch)
tree7381aa654be6284e93c2e0410678eab98fd99568 /doc
parentf0ba692422a8a608ef44964ecf74d8b483c1beb3 (diff)
update Proof General URL
Diffstat (limited to 'doc')
-rw-r--r--doc/faq/fk.bib2
-rw-r--r--doc/refman/RefMan-uti.tex2
-rw-r--r--doc/refman/biblio.bib2
3 files changed, 3 insertions, 3 deletions
diff --git a/doc/faq/fk.bib b/doc/faq/fk.bib
index 4d90efcdb..3410427de 100644
--- a/doc/faq/fk.bib
+++ b/doc/faq/fk.bib
@@ -2171,7 +2171,7 @@ Decomposition}},
@Misc{ProofGeneral,
author = {David Aspinall},
title = {Proof General},
- note = {\url{http://proofgeneral.inf.ed.ac.uk/}}
+ note = {\url{https://proofgeneral.github.io/}}
}
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index c282083b5..10271ce0c 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -251,7 +251,7 @@ to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some
files.
{\ProofGeneral} is developed and distributed independently of the
-system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!.
+system \Coq. It is freely available at \verb!https://proofgeneral.github.io/!.
\section[Module specification]{Module specification\label{gallina}\ttindex{gallina}}
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index 70ee1f41f..e69725838 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -1199,7 +1199,7 @@ Decomposition}},
@Misc{ProofGeneral,
author = {David Aspinall},
title = {Proof General},
- note = {\url{http://proofgeneral.inf.ed.ac.uk/}}
+ note = {\url{https://proofgeneral.github.io/}}
}
@Book{CoqArt,