The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

Hi all,

I'm trying to compile this file: https://gist.github.com/osa1/9615530

I wrote what's happening inside comments but to rephrase,

I can't use constructor name `substx_rec` even though it's not defined
elsewhere(I'm ensuring this using Print command, it says `substx_rec
is not defined`.

Any ideas what's happening?

➜  stagedlambda git:(master) ✗ coqc --version
The Coq Proof Assistant, version 8.4pl2 (June 2013)
compiled on Jun 30 2013 12:15:13 with OCaml 4.00.1

Thanks..

---
Ömer Sinan Ağacan
http://osa1.net