diff options
| author | coqbot-app[bot] | 2021-04-10 18:38:45 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-10 18:38:45 +0000 |
| commit | 7ce1c4844b077adb25d14cf1bbd2d22548b1e935 (patch) | |
| tree | 1bcedda1b36e982295463847391478a0336306c4 | |
| parent | 19e991811dc30bd2392cc969667887a159f355e5 (diff) | |
| parent | b3999ead5497a406653d1ae7c8c7af558d4c6595 (diff) | |
Merge PR #14091: Fix link in doc/cic.rst, there is no Credits chapter anymore
Reviewed-by: jfehrle
| -rw-r--r-- | doc/sphinx/language/cic.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 9f097b4fe9..abe928fa26 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -5,7 +5,7 @@ The underlying formal language of Coq is a :gdef:`Calculus of Inductive Constructions` (|Cic|) whose inference rules are presented in this chapter. The history of this formalism as well as pointers to related -work are provided in a separate chapter; see *Credits*. +work are provided in a separate chapter; see :ref:`history`. .. _The-terms: |