An apply test.
Another fix than 19a7a5789c to avoid descend_in_conjunction to use
fresh names interferring with names later generated in intropatterns
(as introduced in 72498d6d68ac which passed "clenv_refine_in continued
by pattern introduction" to descend_in_conjunction while only a pure
clenv_refine was passed before). The 72498d6d68ac version was
generating fresh names in the wrong order (morally-private names for
descend_in_conjunction before user-level names in clenv_refine_in).
The 19a7a5789c fix was introducing expressions not handled by the
refine from logic.ml.

In particular, this fixes RelationAlgebra.
Fixing bug #3136.

Second-order pattern-matching now respect variable abstraction order.
Adding a test-suite for second-order matching order and indexes.
Cleaning code in Pptactic.

Parametric printers are now using a record to ease the error reporting when
modificating code. Further improvement may include the use of the object
layer of OCaml, which would fit in this particular context.
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