aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorjforest2006-07-17 08:42:00 +0000
committerjforest2006-07-17 08:42:00 +0000
commit324d6e27061689e74c7dafd863fa3d23a8f2716a (patch)
tree379600828ae614d8a2fa2da027d5289dec22e9b3
parent716148d9c71f773699146d1283791ad527b1d4fc (diff)
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9051 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--doc/refman/RefMan-gal.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index f480fc0d2c..8f79af2be1 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1513,7 +1513,7 @@ of \term$_0$.
%Complete!!
The way this recursive function is defined is the subject of several
-papers by Yves Bertot, Julien Forest, David Pichardie.
+papers by Yves Bertot and Antonia Balaa on one hand and Gilles Barthe, Julien Forest, David Pichardie and Vlad Rusu on the other hand.
%Exemples ok ici