This patch was created using

  find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '

and some minor manual editing

This way we avoid the env_cbv tactic unfolding string related stuff
that appears in the goal and hypotheses of the proof mode.

Used in iRevert, iClear, iFrame, and for generalizing the IH in
iInduction and iLöb.

Before, it failed when these tactics were invoked with persistent
hypotheses. The new behavior is more convenient when using these
tactics to build other tactics.

Generating a fresh name consists of two stages:
+ Use [cbv] to compute a list representing the domain of the environment. This
  is a very simply computation that just erases the hypotheses.
+ Use [vm_compute] to compute a fresh name based on the list representing the
  domain. The domain itself should never contain evars, so [vm_compute] will
  do the job.

This reverts commit 3cc38ff6.

The reverted pure hypotheses and variables appear in the wrong order.