Simple simpl

We report on a new implementation of a reduction strategy in Coq to simplify terms during interactive proofs. By "simplify", we mean to reduce terms as much as possible while avoid- ing to make them grow in size. Reaching this goal amounts to a discussion about how not to unfold uselessly global constants. Coq's simpl is such a reduction strategy and the current paper describes an alternative more efficient abstract-machine-based implementation to i