Adding test-suite for bug #3242.
Removing comment outdated since eta holds in conversion rule (this
answers #3299).
Code cleaning in Tacinterp: factorizing some uses of tclEVARS.
Fixing output test-suite: since universe polymorphism, the Print command
shows the polymorphism status of the term.
Fixing test-suite for bug #3043.
Moving Dnet-related code to tactics/.
Adapt the checker to polymorphic universes and projections (untested).
Fast-path equality of sorts in compare_constr*
Avoid allocations in type_of_inductive
- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an evar_map
in tactics, avoiding useless and potentially costly merge's of constraints.
- Implement revert and generalize using the new tactics (not bound to syntax though,
as they are not backwards-compatible yet).
Fix performance problem with unification in presence of universes (bug #3302) by considering
Type i a ground term even when "i" is a flexible universe variable, using the infer_conv
function to do the unification of universes.
Cleanup code in pretyping/evarutil
Little reorganization of generalize tactics code w/o semantic changes.
Also removing trailing spaces.
Renaming new_induct -> induction; new_destruct -> destruct.
Simplification and improvement of "subst x" in such a way that it
works in the presence of local definitions referring to x and
dependent in other hyps or concl.
Isolating a function "make_abstraction", new name of "letin_abstract",
which compute an abstraction of the goal over a term or a pattern.
Typo reference manual
Avoid "revert" to retype-check the goal, and move it to a "new" tactic.
Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic."
(made push command with wrong local ref; leaving control to Matthieu
on new revert)

This reverts commit b797ba85b7b0f82d66af5629ccf6f75d90dda99a.
Encapsulating some clausenv uses. This simplifies the control flow of some
tactics.