Closed andres-erbsen closed 2 years ago
printf '%s\n' '-arg -noinit' > _CoqProject printf '%s\n' 'Set Implicit Arguments.' > a.v vim a.v +CoqToggleDebug +CoqStart +CoqNext
log shows that coqtail tries to run Eval lazy in Prop, but the parsing rule for lazy is not defined yet.
Eval lazy in Prop
lazy
log shows that coqtail tries to run
Eval lazy in Prop, but the parsing rule forlazyis not defined yet.