Code factorization in Tacintern.
Additional entry tactic_arg in Print Grammar tactic.
Cbn in refman
Update RefMan with respect to new loadpath management
Improve RefMan section about Coq_makefile
sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex
Print error messages with more hidden information based on α-equivalence .

The comparison on terms which triggers new printing flags in case two terms which are different would be printed identically now contains α-equivalence.

The implementation using a canonization function on [constr] instead of trying to deal with [constr_expr] was suggested by Hugo.
Code simplification in Tacenv.
Useless hooks in Tacintern.
Fixing bug #2818.

Local Ltac definitions do not register their name in the nametab anymore,
thus elegantly solving the bug. The tactic body remains accessible from
the tactic engine, but the name is rendered meaningless to the userside.
Test-suite for bug #2818.
Fixing printing of unreachable local tactics.
Yes another remaining clearing bug with 'apply in'.
Putting back normalized goals when entering them.

This should allow tactics after a Goal.enter not to have to renormalize
them uselessly.