diff options
| author | Tanaka Akira | 2019-02-08 11:34:43 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-02-08 11:34:43 +0900 |
| commit | 613b9ee88067392b7681ee5f0c28d5c5cfff6276 (patch) | |
| tree | c5e42889cc25f205b2400cbd6128b6080f5be790 | |
| parent | ca40e534580a67ca327b5f1b054e4089ac2ee281 (diff) | |
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.
| -rw-r--r-- | doc/sphinx/language/cic.rst | 4 |
1 files 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}]`. |