aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/common/title.tex
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-01-20 17:25:10 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-01-20 17:33:09 +0100
commit86f5c0cbfa64c5d0949365369529c5b607878ef8 (patch)
treefadba5223c85fda1c0586b1ebed33c84420cff61 /doc/common/title.tex
parentaf5eafaee218935c35f0bd906727d2d2370bd136 (diff)
Update copyright headers.
Diffstat (limited to 'doc/common/title.tex')
-rw-r--r--doc/common/title.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/common/title.tex b/doc/common/title.tex
index 4716c3156..0e072b6b6 100644
--- a/doc/common/title.tex
+++ b/doc/common/title.tex
@@ -45,7 +45,7 @@ V\coqversion, \today
%END LATEX
\copyright INRIA 1999-2004 ({\Coq} versions 7.x)
-\copyright INRIA 2004-2015 ({\Coq} versions 8.x)
+\copyright INRIA 2004-2016 ({\Coq} versions 8.x)
#3
\end{flushleft}