The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

For example, defining pred as below, using the name "plus" as a matching 
variable (where "plus" is also a predeclared function), means that in the 
body of the successor case, you cannot use "plus" as the addition function.

Definition mypred := [n:nat] (Cases n of O => O | (S plus) => plus end).
Warning: Defined reference plus is here considered as a matching variable

--- nadeem


Eduardo Gimenez wrote:

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


-------------------
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/