The Coq mailing list

[Laurent Th�ry <Laurent.Thery AT inria.fr>]

> No, I meant coqtop. Problem is so demanding and proof take so much time
> because it's problem within Presburger arithmetic which I try to solve
> using omega. It use many hypothesis and axioms. Problem is provable. I
> have proved it in theory!


Unfortunately omega is based on fourier elimination so is very sensitive to
the number of equations.
Just to be sure that it is a problem of exponentiel blow-up can you try
with the lia tactic (Require Import Psatz) to see if this crashes too?

--
Laurent Théry