First stab at documenting Canonical Structures
Tentative fix to recover fresh name generation as it was before
new-tacticals merge. This is essentially a revert of 6fea2f which
broke the sacrosanct backward compatibility of name generation,
thus breaking quite a lot of contribs.
Useless instantiation function exported in Evd.
Better heuristic for name generation backward compatibility. We fallback
to old behaviour whenever we were in Program mode.
Getting rid of casted_open_constr. It was only used by the
refine tactic, which now uses plain glob_constr's. Now there
is no real need to depend on goal when interpreting genargs.

Possible minor incompatibilities:

1. The interpretation of glob_constr to constr is now done by
Goal.constr_of_raw, which may be slightly dumbier than the dedicated
Tacinterp.interp_open_constr which tries harder. Stdlib and test-suite
do go through, though.

2. I had to change the parsing level of wit_glob in Extraargs
from lconstr to constr. It may break ML notations using glob, but
as they are only used inside Coq code and all well-parenthezised,
it should be OK.
Adding printing of ltac envs to debugger.
Fixing ltac constr variable handling in refine.
Ensuring the right parsing of glob arguments, used by refine
and instantiate. Each of these tactics uses it at a different
parsing level, thus actually triggering a parsing error after
merging them. This fix implies some code duplication, which is
a pity. The separation between genargs and parsing entries should
be made one day.
Removing RefArgType generic argument.
Print logical name rather than path (thus allowing reproducible tests).
Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr//gitroot/coq/coq into trunk
Test suite: update output reference.
Writing [cut] tactic using the new monad.
Porting type interpretation in Tacinterp to the new tactics.
Test case for bug#2848.