Fix Declaremods.end_library (Closes: #3536)
coqworkmgr
stm: use xlabel insted of label in dot (debug) output
Removing [revert] tactic from the AST.
Fixup introduction of coqworkmgr
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.