aboutsummaryrefslogtreecommitdiff
path: root/doc/common/title.tex
diff options
context:
space:
mode:
authorThéo Zimmermann2019-06-06 11:22:09 +0200
committerThéo Zimmermann2019-06-17 18:08:33 +0200
commitffd9b12fe9e279fa896fc7e89d4f4d26c260ddfc (patch)
treeb1a999a1ad46f97b870dfa14bd9d978369e54e8c /doc/common/title.tex
parent2ec2affa73720746bef37e8b1f0ce98f257cb302 (diff)
Update copyright years outside of headers.
These were found with the following command: $ git grep "1999-" | grep -v "2019"
Diffstat (limited to 'doc/common/title.tex')
-rw-r--r--doc/common/title.tex4
1 files changed, 1 insertions, 3 deletions
diff --git a/doc/common/title.tex b/doc/common/title.tex
index 76e50f65d2..2a104a87e6 100644
--- a/doc/common/title.tex
+++ b/doc/common/title.tex
@@ -43,9 +43,7 @@ $\pi r^2$ Project (formerly LogiCal, then TypiCal)
V\coqversion, \today
\par\vspace{20pt}
%END LATEX
-\copyright INRIA 1999-2004 ({\Coq} versions 7.x)
-
-\copyright INRIA 2004-2017 ({\Coq} versions 8.x)
+\copyright 1999-2019, Inria, CNRS and contributors
#3
\end{flushleft}