Fix change: nf_evar prior to tactic interpretation.

Noticed in PTSATR.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17056 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix the tactical ; [ … ] : the "incorrect number of goal" error was not caught by ltac tacticals.

The errors were not translated into ltac errors (and at some occurence errors were raised in OCaml rather than inside the tactic monad).

Spotted in ProjectiveGeometry and Goedel.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17057 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix ltac's progress tactical: requires progress in each goal.

Proofview.tclPROGRESS considers that a tactic that changes the list of goal progresses, under this semantics, "progress auto" succeeds if its applied to two goals and solves the first one but not the second one. This would break backwards compatibility.

Spotted in Fermat4.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17058 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was solved.

This made "autorewrite using tac" fail.

Spotted in CoLoR and Demos.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17059 85f007b7-540e-0410-9357-904b9bb8a0f7
Nicer infered names in refine.

When an existential variable is created, the rel context becomes a named context, and identifiers are given to anonymous variables. Instead of using an identifier based on "H" all the time, use an identifier based on the lower case first letter of the type.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17060 85f007b7-540e-0410-9357-904b9bb8a0f7