Added link to CtCoq

1 files changed, 15 insertions, 1 deletions

diff --git a/html/links.phtml b/html/links.phtml
index 044fd1b9..87fb489c 100644
--- a/html/links.phtml
+++ b/html/links.phtml
@@ -7,7 +7,7 @@ for links to include here, or find broken links, please
 </p>
 
 <ul>
-<li><a href="http://www.dcs.ed.ac.uk/home/da/Isamode">Isamode</a>
+<li><a href="http://zermelo.dcs.ed.ac.uk/~isamode">Isamode</a>
   is an XEmacs front-end for Isabelle.  It has a different
   feature collection compared with Proof General:
   script management is not supported, but there are extensive
@@ -15,3 +15,17 @@ for links to include here, or find broken links, please
   commands.
 </li>
 </ul>
+<ul>
+<li><a href="http://www-sop.inria.fr/croap/ctcoq/ctcoq-eng.html">CtCoq</a>
+  is an interface for the Coq theorem prover, developed
+  at INRIA, Sophia Antipolis as part of
+  <a href="http://www-sop.inria.fr/croap/">Projet CROAP</a>.
+  Like Proof General, CtCoq is based on a general approach for
+  building user-interfaces for theorem provers, although no other
+  current theorem provers are supported.  Unlike Proof General, CtCoq
+  is based on a graphical environment with structure editing,
+  created with the <a
+  href="http://www-sop.inria.fr/croap/centaur/centaur.html">Centaur</a>
+  system.
+</li>
+</ul>