aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-25 09:56:20 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-25 09:56:20 +0000
commit97d7b5ee7c122681b82723c90115b98ddc09b996 (patch)
tree99cc3afbe53959fb9ea9454b22f46aae6cd6b2eb
parenta3fc112d0e3ae5fe3ae6179596e5e2aa6275ef2e (diff)
Fixed #2789.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15360 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--COPYRIGHT2
-rw-r--r--CREDITS2
-rw-r--r--doc/refman/RefMan-pre.tex4
3 files changed, 4 insertions, 4 deletions
diff --git a/COPYRIGHT b/COPYRIGHT
index 4efe90590..a98eed3d1 100644
--- a/COPYRIGHT
+++ b/COPYRIGHT
@@ -7,7 +7,7 @@ This product includes also software developed by
Pierre Crégut, France Telecom R & D (plugins/omega and plugins/romega)
Pierre Courtieu and Julien Forest, CNAM (plugins/funind)
Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml)
- Pierre Corbineau, Radbout University, Nijmegen (declarative mode)
+ Pierre Corbineau, Radboud University, Nijmegen (declarative mode)
John Harrison, University of Cambridge (csdp wrapper)
The file CREDITS contains a list of contributors.
diff --git a/CREDITS b/CREDITS
index 543cb3f39..35057ea8f 100644
--- a/CREDITS
+++ b/CREDITS
@@ -65,7 +65,7 @@ plugins/subtac
plugins/xml
developed by Claudio Sacerdoti (Univ. Bologna, 2000-2005)
as part of the HELM and MoWGLI projects; extension by Cezary Kaliszyk as
- part of the ProofWeb project (Radbout University at Nijmegen, 2008)
+ part of the ProofWeb project (Radboud University at Nijmegen, 2008)
plugins/micromega
developed by Frédéric Besson (IRISA/INRIA, 2006-2008), with some
extensions by Evgeny Makarov (INRIA, 2007); sum-of-squares solver and
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 7159fc0b2..6d23f02f2 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -586,7 +586,7 @@ language, usable in combination with the tactic-based style of proof.
Finally, many users suggested improvements of the system through the
Coq-Club mailing list and bug-tracker systems, especially user groups
-from INRIA Rocquencourt, Radbout University, University of
+from INRIA Rocquencourt, Radboud University, University of
Pennsylvania and Yale University.
\enlargethispage{\baselineskip}
@@ -683,7 +683,7 @@ improved the libraries of integers, rational, and real numbers. We
also thank many users and partners for suggestions and feedback, in
particular Pierre Castéran and Arthur Charguéraud, the INRIA Marelle
team, Georges Gonthier and the INRIA-Microsoft Mathematical Components team,
-the Foundations group at Radbout university in Nijmegen, reporters of bugs
+the Foundations group at Radboud university in Nijmegen, reporters of bugs
and participants to the Coq-Club mailing list.
\begin{flushright}