Correct W-Ind.

Remove the 2nd premise "(E[Γ_P ] ⊢ A_j : s_j)_(j=1...k)".
Also, "Γ" in "c_i ∉ Γ ∪ E" is changed to "Γ_I".

"E[Γ_P ] ⊢ A_j : s_j" contradicts with a side condition
"A_j is an arity of sort s_j".
The latter means that A_j is ∀ x1:T1, ... ∀ xm:Tm, s_j.
So, "(∀ x1:T1, ..., s_j) : s_j)" is required.
Using Prod-{Prop,Set,Type}, it needs "s_j : s_j" which cannot be proved.

This problem is introduced at 2018-07-22:
https://github.com/coq/coq/commit/f25c1d252ad61b4dc4321e3a11f33b1e6d4e3dff
Before that, the premise describes "A_j : s'_j".
And "s'_j" is not explained anywhere.

I think "A_j : s'_j" describes that A_j is a type (a value of a sort).
Thus, "A_j is an arity of sort s_j" imply "A_j : s'_j".

So, I removed the 2nd premise.

Also, a side condition describes "c_i ∉ Γ ∪ E" but "Γ" is not explained.
I think that Γ should be Γ_I.

Γ should include Γ_I because a constructor, c_i, and inductive types are
both defined in global environment and it cannot accept duplicate name.
Actually, such definition fails:

```
Fail Inductive X := X : X.
(* The following names are used both as type names and constructor names: X.*)
```

Γ doesn't include Γ_P because parameters are not defined in global
environment.
Actually, a parameter can be same name as a constructor name:

```
Inductive I (X : nat) := X : I X.
Check X. (* X : forall X : nat, I X *)
```

1 files changed, 1 insertions, 2 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 67683902cd..ae6ca18f92 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -963,7 +963,6 @@ such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;~…;~I_k :∀ Γ_P ,A_k]`
 .. inference:: W-Ind
 
    \WFE{Γ_P}
-   (E[Γ_P ] ⊢ A_j : s_j )_{j=1… k}
    (E[Γ_I ;Γ_P ] ⊢ C_i : s_{q_i} )_{i=1… n}
    ------------------------------------------
    \WF{E;~\ind{p}{Γ_I}{Γ_C}}{Γ}
@@ -976,7 +975,7 @@ provided that the following side conditions hold:
       context of parameters,
     + for :math:`j=1… k` we have that :math:`A_j` is an arity of sort :math:`s_j` and :math:`I_j ∉ E`,
     + for :math:`i=1… n` we have that :math:`C_i` is a type of constructor of :math:`I_{q_i}` which
-      satisfies the positivity condition for :math:`I_1 … I_k` and :math:`c_i ∉ Γ ∪ E`.
+      satisfies the positivity condition for :math:`I_1 … I_k` and :math:`c_i ∉ Γ_I ∪ E`.
 
 One can remark that there is a constraint between the sort of the
 arity of the inductive type and the sort of the type of its