Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? Does the user mean "Unfold X.t" or does she mean "Unfold y" where X.t is later on instantiated with y? I choose the first interpretation (i.e. an evaluable reference is never expanded).

Fails on opaque constants and variables (both those without bodies and those marked Opaque in the conversion oracle).

Succeeds for any constant or variable even if marked opaque or otherwise not evaluable.

Red (returns None if nothing reducible)

Simpl

Simpl only at the head

Hnf: like whd_simpl but force delta-reduction of constants that do not immediately hide a non reducible fix or cofix

Variant of the above that does not perform nf-βι

Unfold

Fold

Pattern

Call by value strategy (uses Closures)

= cbv_betadeltaiota

reduce_to_atomic_ind env sigma t puts t in the form t'=(I args) with I an inductive definition; returns I and t' or fails with a user error

reduce_to_quantified_ind env sigma t puts t in the form t'=(x1:A1)..(xn:An)(I args) with I an inductive definition; returns I and t' or fails with a user error

Same as reduce_to_quantified_ind but more efficient because it does not return the normalized type.

reduce_to_quantified_ref env sigma ref t try to put t in the form t'=(x1:A1)..(xn:An)(ref args). When this is not possible, if allow_failure is specified, t is unfolded until the point where this impossibility is plainly visible. Otherwise, it fails with user error.

Errors if the inductive is not allowed for pattern-matching. *