The Coq mailing list

[Carmine Abate <carmine.abate AT inria.fr>]

Hi everybody, 

can some-one tell me how does Coq write the term α_ind

(and eventually α_rect) for a generic inductive type α, like the following? 

Inductive α (b₁ : B₁) .. (bᵤ : Bᵤ) : ∏_{ z₁ : Q₁ .. zₘ : Qₘ} s := 

 | c₁ : ∏_{x₁ : P₁₁ .. xₖ₁ : P₁ₖ₁} α (b₁ : B₁) .. (bᵤ : Bᵤ) M₁₁ .. M₁ₘ 

    ...

 | cₙ : ∏_{x₁ : Pn₁ .. xₖₙ : P₁ₖₙ} α (b₁ : B₁) .. (bᵤ : Bᵤ) Mₙ₁ .. Mₙₘ