gmalecha / template-coq

Reflection library for Coq
MIT License
12 stars 0 forks source link

Handle section variables correctly #3

Closed gmalecha closed 10 years ago

gmalecha commented 10 years ago

There are three possibilities:

1) Reject quoting within a section 2) Replace the terms with functions from terms to terms for each variable in the context. 3) Abstract at the level of terms, i.e. add an extra [Lambda] constructor.

Only the first is sound.

gmalecha commented 10 years ago

Closed in 7ca4024