Fixing confused code for interpretations of evar instances.
Now that evars can be parsed, protect strongly Check from calling kernel with evars.
New bugs revealed fixed: #3408 by (probably) Maxime's commits
on vm and #3068 by Nov 2 commit on destruct.

Also fixed test for failure of #3459.
Writing rename_hyps in the new monad.

This new implementation now allows for simultaneous replacing of hypotheses,
thus fixing bug #2149.
Test for bug #2149.