Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] available context in refine 'holes'

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] available context in refine 'holes'


chronological Thread 
  • From: "Kouskoulas, Yanni A." <Yanni.Kouskoulas AT jhuapl.edu>
  • To: Adam Chlipala <adamc AT hcoop.net>
  • Cc: "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>
  • Subject: RE: [Coq-Club] available context in refine 'holes'
  • Date: Sun, 11 Jan 2009 11:56:27 -0500
  • Accept-language: en-US
  • Acceptlanguage: en-US
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Thanks for the quick reply, Adam! 

Your explanation makes sense. I will look into better understanding dependent 
match annotations.

And you already know I am looking at your textbook. :)

-Yanni





Archive powered by MhonArc 2.6.16.

Top of Page