The Coq mailing list

[guninski AT guninski.com]

"Anomaly" when doing Load self.v

a file named "self.v" having:
Load self.
results in:

Anomaly: uncaught exception Sys_error "/tmp/self.v: Too many open files".
Please report.


please excuse my dumbness:

is normal behavior invoking a lemma to break the future proof of the true 
fact:
"True -> True" (implication).

the lemma magically changes the coq subgoal from True to False after invoking
the lemma. (if i can change it the other way, i will have a fake proof).

is there some theoretical justification the subgoal to be changed to False at
will?

i can give a very short testcase.

thanks.