Ssreflect Users Discussion List

[Guillaume Melquiond <>]

On 22/02/2016 20:52, Ralf Jung wrote:
> It seems that it's always the first occurrence that has to have the "[",
> like that's some kind of binder that completely transcends the AST...
> weird.

On 22/02/2016 21:03, Pierre-Yves Strub wrote:
> But in Guillaume's mail, it seems that there is a dissymmetry between
> the 2 evars (namely ?[n] and ?n). Is only one is subject to
> instantiation ?

No, the ?[n] syntax creates an evar named n, while the ?n syntax uses
the evar named n. Using twice ?n would not work since there are no evar
named n; using twice ?[n] would not work since there would be a name
conflict. So the first evar encountered by Coq (in application order)
needs to be ?[n], and the subsequent ones are ?n.

Best regards,

Guillaume