diff options
| author | Tanaka Akira | 2019-02-08 10:40:19 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-02-08 10:40:19 +0900 |
| commit | 12a5f48cff9508a0fe42856762e116bb92c1c61a (patch) | |
| tree | 2ebf86b09f62dff2e0f758d280cfff881a2277a6 | |
| parent | 7886c6d8e0663ba346fff52837012c7fc952ecc1 (diff) | |
Remove "'" accidentaly added.
"'" in the extended (k_i added) form of Fix syntax should be removed.
In the following sentence, A_i' is referenced as A_i.
```
Each :math:`A_i` should be a type (reducible to a term) starting
with at least :math:`k_i` products
:math:`∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i'`
```
Also, A_i' is used in ∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i' and
A_i' must not equal to ∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i'.
The old reference manual, coq-8.7.2-reference-manual.pdf,
doesn't have "'".
They are added by
https://github.com/coq/coq/commit/47dca6c5da585212f69b6b83b25896ff990781e3
which ports Cic document from TeX to sphinx.
So, the change seems just an accident.
| -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 962d2a94e3..b56f0cc9e3 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1632,7 +1632,7 @@ should be an inductive definition. For doing this, the syntax of fixpoints is extended and becomes .. math:: - \Fix~f_i\{f_1/k_1 :A_1':=t_1' … f_n/k_n :A_n':=t_n'\} + \Fix~f_i\{f_1/k_1 :A_1:=t_1 … f_n/k_n :A_n:=t_n\} where :math:`k_i` are positive integers. Each :math:`k_i` represents the index of |