The Coq mailing list

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

  Hi,

> What is the meaning of this warning and which command raises it up??
>
> "Warning: Defined reference data is here considered as a matching variable"

  It means that the name "data" denotes a defined or declared object
(inductive, constant or section variables - but not a constructor) but
is considered as a binding variable in the current pattern.

  Hugo
-------------------
To unsubscribe, mail 
coq-club-request AT pauillac.inria.fr
Bug reports: http://coq.inria.fr/bin/coq-bugs
Coq-Club Archives: http://coq.inria.fr/mailing-lists/coqclub/