The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

Hi,

I have a relative small development that is composed of only
simple functions inside sections.
Coq is really really slow to typecheck it.
The file is in
ftp://ftp-sop.inria.fr/lemme/Laurent.Thery/coq-test.v
and takes 8 minutes to compile on my machine!

The problem seems to come from the typing of a match (an if)
of the following function:

Fixpoint remove_elem (e: PExpr C) (l: list (PExpr C)) {struct l}: option 
(list (PExpr C)) :=
match l with
   nil   =>  None
| cons e1 l1  =>
   if (test_in e e1) then Some l1 else (ocons e1 (remove_elem e l1)) 
end.

I have a quick fix

Definition id_bool: bool -> bool.
intro x; exact x.
Qed.

Fixpoint remove_elem (e: PExpr C) (l: list (PExpr C)) {struct l}: option 
(list (PExpr C)) :=
match l with
   nil   =>  None
| cons e1 l1  =>
   if id_boo (test_in e e1) then Some l1 else (ocons e1 (remove_elem e 
l1)) 
end.

now the compiling time drops to 1 second but I've lost evaluation
inside Coq.

Is there a way I can get both quick compilation and evaluation inside
Coq?

--
Laurent Théry