The Coq mailing list

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

Hi,

I'm getting more and more puzzled by Coq behaviour. Here is an
example:

I've a function that is computationally very intensive:

Definition myfun (x: nat): option nat := ..

Then when I do

Eval vm_compute in myfun 1.
     = Some 25011
     : option nat
Finished transaction in 35. secs

Ok fine, but when I do

Eval vm_compute in (match myfun 1 with Some c => c | None => O end).

This never returns.

Why? Actually this is a typechecking problem: in order to typecheck
the expression, it seems that Coq tries to normalize the term (myfun 10), 
no way it will  succeed without the vm_compute.

Ok my example is a bit contrived. But here is the actual
situation where I got the bug.

I had defined this tactic:

Ltac mytac l :=
  let x := eval vm_compute in
     match myfun l with
      Some c => c
    | None   =>  ..
    end in
           .....

and now while proving a theorem, I call the tactic

mytac 1.

and this loops: the term (match myfun 1 .... end) is created and 
typechecked dynamically by Ltac :-(

Here is my question:
Is there a real good reason for having this unrestricted normalisation in
the typechecking?

--
Laurent Théry