Passing some tactics to the new monad type.
Code cleaning in Univ.
Adapt simpl/cbn unfolding and refolding machinery to projections, so that
primitive projections obey the Arguments command.
Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).
Check resolution of Metas turned into Evars by pose_all_metas_as_evars
in unification.ml in case prefix 'e' of "apply" and co is not given.
Improved error message when a meta posed as an evar remains unsolved
in case prefix 'e' of "apply" and co is not given.
Fixing "clear" in internal_cut_replace: forbid dependencies in the
name of replaced hypothesis.
Improving tclWITHHOLES which did not see undefined evars up to
restriction, after last fix commit which precisely possibly restricts
evars of a term "t" in "apply t in H" without resolving them.
Less ocaml warnings.