aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-12 20:24:52 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-12 20:24:52 +0200
commit0f68627e37357f7ff37dba59abb856c52b411830 (patch)
tree8a8200930bfb261a480973b0b12b1da8e00b6789 /doc
parent424cffe91ee8819de8cde27d98c534eed51ca251 (diff)
parentc91f9c180fda584be0fb5b068243c44cf1374a62 (diff)
Merge PR #7222: [sphinx] Remove migration artefacts.
Diffstat (limited to 'doc')
-rw-r--r--doc/sphinx/addendum/miscellaneous-extensions.rst3
-rw-r--r--doc/sphinx/addendum/type-classes.rst3
-rw-r--r--doc/sphinx/language/coq-library.rst3
-rw-r--r--doc/sphinx/proof-engine/ssreflect-proof-language.rst5
4 files changed, 1 insertions, 13 deletions
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst
index b0343a8f0..3ed4ce762 100644
--- a/doc/sphinx/addendum/miscellaneous-extensions.rst
+++ b/doc/sphinx/addendum/miscellaneous-extensions.rst
@@ -5,9 +5,6 @@
Miscellaneous extensions
=======================
-:Source: https://coq.inria.fr/distrib/current/refman/miscellaneous.html
-:Converted by: Paul Steckler
-
.. contents::
:local:
:depth: 1
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index becebb421..5518da9ac 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -5,9 +5,6 @@
Type Classes
============
-:Source: https://coq.inria.fr/distrib/current/refman/type-classes.html
-:Author: Matthieu Sozeau
-
This chapter presents a quick reference of the commands related to type
classes. For an actual introduction to type classes, there is a
description of the system :cite:`sozeau08` and the literature on type
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 29053d6a5..82ced65b4 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -5,9 +5,6 @@
The |Coq| library
=================
-:Source: https://coq.inria.fr/distrib/current/refman/stdlib.html
-:Converted by: Pierre Letouzey
-
.. index::
single: Theories
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index bd71e5ed8..df5b36297 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -6,10 +6,7 @@
The |SSR| proof language
------------------------------
-:Source: https://coq.inria.fr/distrib/current/refman/ssreflect.html
-:Converted by: Enrico Tassi
-
-Author: Georges Gonthier, Assia Mahboubi, Enrico Tassi
+:Authors: Georges Gonthier, Assia Mahboubi, Enrico Tassi
Introduction