The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

[firstorder] hangs both coqtop and coqc consuming memory on this testcase:

Inductive AA : Prop := A0: forall B : Prop, AA->B->AA.
Lemma l1: AA->False.
Proof.
(* apply AA_ind. intros. contradiction. *)
firstorder.
Qed.

i doubt this is possible, but can i port this to the .vo or is it just a .ml 
plugin feature?

-- 
joro