Skip to Content.
Sympa Menu

coq-club - [Coq-Club] "function" is opaque.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] "function" is opaque.


chronological Thread 
  • From: Dimitris Vekris <dvekris AT hotmail.com>
  • To: <coq-club AT pauillac.inria.fr>
  • Subject: [Coq-Club] "function" is opaque.
  • Date: Thu, 16 Jul 2009 11:21:02 +0300
  • Importance: Normal
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello everyone.

I am trying to unfold a function that I have written in 'proof mode' and I am getting this error. I know that you get this when for example you have:

Variable f: A -> B.

Theorem bla_bla.
...
unfold f.

But this is not my case. What may be the reasons for this kind of error?

Thanks!

Dimitris





check out the rest of the Windows Live™. More than mail–Windows Live™ goes way beyond your inbox. More than messages



Archive powered by MhonArc 2.6.16.

Top of Page