The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

Le 25/05/2011 17:33, David Baelde a écrit :
> OCaml applications compiled to native code may cause segmentation
> faults as a result of stack overflows. I have experienced this,
> including with Coq, for which I have a file that causes sigsegv or
> stack overflow depending on the coq/ocaml versions:
> 
> Require Export Bvector.
> Notation BVfalse := (Vconst bool false).
> Goal forall n (a b : bool) (v : Bvector n),
>       Vcons _ a n v = Vcons _ b n (BVfalse n) -> v = BVfalse n.
> Proof.
>   intros.
>   assert (v = BVfalse n) by congruence.
> 
> Cheers,

No need to go that far. "Check 100000." usually suffices.


Cheers,

-- 
Stéphane