The Coq mailing list

[Luke Palmer <lrpalmer AT gmail.com>]

I'm fairly new to Coq (have been for a couple years ;-), trying to get
a feel for well-founded recursion.  I have defined this program using
Russell:

Definition id A (x:A) := x.

Program Fixpoint bottom (n:nat) { measure (id nat) } :=
 match n with
 | O => O
 | S n => S (bottom (S n))
 end.
Next Obligation. Admitted.

Compute bottom 2.

I'm wondering how Coq manages not to get into an infinite loop here.
It shows me some ghod-awful gnarly term instead, as if it got stuck
evaluating the admitted obligation.  What confuses me is that the
program:

Program Fixpoint div2 (n:nat) { measure (id nat) } :
 match n with
 | O => O
 | S O => O
 | S (S n) => S (div2 n)
 end.
Next Obligation. Admitted.

Compute div2 100.

Manages to reduce to normal form just fine.  What mechanism is causing
Coq to stop evaluating bottom, but not div2?

Thanks,
Luke