aboutsummaryrefslogtreecommitdiff
path: root/doc/common
diff options
context:
space:
mode:
authorMaxime Dénès2017-08-31 13:20:42 +0200
committerMaxime Dénès2017-08-31 13:20:42 +0200
commitbed414f560e3db511ca3a647acce6e5ebc70b4cc (patch)
treee38aa2b525eac9c97a55f0c993fae338b756e26e /doc/common
parentce2b0bb105e1e6652a66df2160bd86b3ffdc175d (diff)
parent972877ba4d81fca11d762d73c140ea590aeec48b (diff)
Merge PR #993: Credits for version 8.7
Diffstat (limited to 'doc/common')
-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 0e072b6b65..76e50f65d2 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-2016 ({\Coq} versions 8.x)
+\copyright INRIA 2004-2017 ({\Coq} versions 8.x)
#3
\end{flushleft}