The Coq mailing list

[roconnor AT theorem.ca]

Coq needs to evalutate the witness of termination into some sort of head 
normal form before proceeding with one step of recursion.  Coq wants to 
verify that your proof of termination isn't ``hypothetical'' by making 
sure that the normal form begins with a constructor.  This means that your 
proof of termination needs to be sufficently transparent and cannot have 
axioms that end up at the head position of the witness of termination.

Making sure that the witness of termination isn't hypothetical ensures 
that Coq will not go into an infinte loop when evalutating a recursive 
function inside an inconsistent context (such an inconsistency could arise 
from axioms or from variables or hypothesis of functions).

In theory Coq is not going into an infinite loop in your latter case. 
Evalutation of the fixpoint presumably gets stuck when the head of the 
witness of termination becomes an axiom of classical logic rather than a 
constructor.  Then compute proceeds to put the rest of your proof into 
normal form by eliminating cuts.  I'm not sure how many hours, days, or 
years it will take for Coq to finish normalizing the remainder of your 
proof, nor do I know how much memory will be used by the normalized proof.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''