The Coq mailing list

[Vincent Demange <vincent.demange AT ensiie.fr>]

Le lundi 17 juin 2013 à 18:33 -0700, Math Prover a écrit :
> 
>   I have one question about your example: I don't understand what
> "constr:" means.
I use "constr:" prefix to build Galline terms.


If I used "cons P lQ" in a tactic instead of "constr:(cons P lQ)" then
Coq would have complained because cons is not the name of a tactic.

It is well explained in Adam's book that you quoted:
http://adam.chlipala.net/cpdt/html/Match.html#lab90
> 

Cheers,
Vincent.