The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 19/11/2014 14:50, 
michael.soegtrop AT intel.com
 wrote:
> Record A:=mkA
> {
>    a := 1
> }.
>
> (* The induction principle for this actually works *)
>
> Lemma TestIndA : forall x:A, a x =1.
> Proof.
>    induction x.
>    reflexivity.
> Qed.
>
> (* But when I print the induction principle, I get this *)
>
> Print A_rect.
>
> A_rect =
> fun (P : A -> Type) (f : let a := 1 in P mkA) (a : A) =>
> match a as a0 return (P a0) with
> | {| a := x |} => f x
> end
>       : forall P : A -> Type, (let a := 1 in P mkA) -> forall a : A, P a

That is a plain bug of the Coq printer. The actual induction principle 
should be something like

fun (P : A -> Type) (f : let a := 1 in P mkA) (a : A) =>
  match a as a0 return (P a0) with
  | mkA => f
  end

I suggest reporting it on the bug tracker.

Best regards,

Guillaume