From 12a5f48cff9508a0fe42856762e116bb92c1c61a Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Fri, 8 Feb 2019 10:40:19 +0900
Subject: 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.
---
 doc/sphinx/language/cic.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3