From 613b9ee88067392b7681ee5f0c28d5c5cfff6276 Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Fri, 8 Feb 2019 11:34:43 +0900
Subject: Change c to c' forgotten at exchanging c and c'.

In Cic admissible rules section, c and c' are exchanged at
https://github.com/coq/coq/commit/8654b03544f0efe4b418a0afdc871ff84784ff83 .

But the exchange is not complete.
This commit complete it.
---
 doc/sphinx/language/cic.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 4e3b981c58..5392552878 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1750,7 +1750,7 @@ One can modify a global declaration by generalizing it over a
 previously assumed constant :math:`c`. For doing that, we need to modify the
 reference to the global declaration in the subsequent global
 environment and local context by explicitly applying this constant to
-the constant :math:`c'`.
+the constant :math:`c`.
 
 Below, if :math:`Γ` is a context of the form :math:`[y_1 :A_1 ;~…;~y_n :A_n]`, we write
 :math:`∀x:U,~\subst{Γ}{c}{x}` to mean
@@ -1780,7 +1780,7 @@ and :math:`\subst{E}{|Γ|}{|Γ|c}` to mean the parallel substitution
          {\subst{Γ}{|Γ_I ;Γ_C|}{|Γ_I ;Γ_C | c}}}
 
 One can similarly modify a global declaration by generalizing it over
-a previously defined constant :math:`c′`. Below, if :math:`Γ` is a context of the form
+a previously defined constant :math:`c`. Below, if :math:`Γ` is a context of the form
 :math:`[y_1 :A_1 ;~…;~y_n :A_n]`, we write :math:`\subst{Γ}{c}{u}` to mean
 :math:`[y_1 :\subst{A_1} {c}{u};~…;~y_n:\subst{A_n} {c}{u}]`.
 
-- 
cgit v1.2.3