Issues
- 3
template-coq does not build with Coq master
#44 opened by JasonGross - 2
Anomaly: Uncaught exception Reify.TermReify.NotSupported(_). Please report at http://coq.inria.fr/bugs/.
#39 opened by JasonGross - 7
Reification of Universes!
#1 opened by gmalecha - 0
- 3
elaboration/type inference while unquoting
#36 opened by aa755 - 2
Use common code in PluginUtils
#34 opened by gmalecha - 4
- 4
ExtLib dependency for monads notations
#33 opened by aa755 - 3
Port to Coq8.6
#30 opened by yforster - 4
Quoting function is slow when quoting itself.
#11 opened by JasonGross - 2
Breaking changes in Coq 8.5~beta3
#21 opened by clarus - 4
unquoting changes Prop to Set
#28 opened by aa755 - 4
Turn "Make Definition" into a tactic
#18 opened by yforster - 4
- 2
- 5
- 3
`make install` fails
#8 opened by JasonGross - 5
Compatibility with coq-8.5
#7 opened by yforster - 1
Check the quoting of mutual fixpoints
#6 opened by gmalecha - 1
Support quoting of opaque symbols
#5 opened by gmalecha - 1
Quoting of inductive types
#4 opened by gmalecha - 1
Handle section variables correctly
#3 opened by gmalecha - 1
Recursive Reification
#2 opened by gmalecha