The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

On Sat, Sep 30, 2017 at 02:22:47AM +0200, Anders Lundstedt wrote:
> Reserved Notation "* a" (at level 70).
> Inductive P {n : nat} : nat -> Prop :=
> | c1 m : P m
> | c2 m : *m
> where "* m" := (P m).
> 
> Why do I get an error "Cannot infer the implicit parameter n of P ..."
> for constructor c2 but not for constructor c1?

This is a (known) limitation of the combination of "Inductive",
"where" and implicit parameters. The current workaround is to declare
either the implicit parameters, or the notation in a second step.

You could fill a bug report so that something is eventually done to
improve this. Sorry about this restriction.

Best regards,

Hugo Herbelin