A dependent substitution is a substitution from formulae to formulae
that can act depend on the topmost universally quantified variables of
the formula.  This is going to be useful for handling substitutions of
clauses.

This structure is intended to be used for resolution and
paramodulation tactics. Having both clauses under the same quantifiers
allows to perform shallow unification.

This is intended to help debugging failure of the "assumption"
certificate combinator and similar ones built on top of with_variable
and with_assumption.  The user can herself see why the goal is not one
of the assumptions.

The configure script can be called with --with-confluence-checking for
forcing confluence checking.

This reverts commit 1dad75e6.

Conflicts:
	configure

In Dedukti v2.6, we can now declare term as injective so the user can
handle higher-order logic by adding injective rewrite rules on term.

containing injective symbols)

The main motivation is to ease integration into higher-order logic
which would orhterwise require fol.term to be a definable
symbol (which poses injectivity problems).

This change requires -coc, and the latest (v2.5.1) versions of Dedukti
and Meta Dedukti (because -coc was not present before in Meta
Dedukti). fol.term is now defined as the identity over types so it is
not mandatory to remove it from the developments but fol.type needs to
be replaced by Type since Dedukti does not allow kind-level
definitions.

A new bug has been discovered (#21276). It has been triggered by the
eqcert.match_f_equal_goal function and has required to remove the
eqcert.f_equal certificate transformer.

The script dktactics get installed in INSTALL_BIN_DIR; its only
purpose is to print the path INSTALL_LIB_DIR in which the dko files
are installed.

This corresponds to my presentation at
LSV (http://deducteam.gforge.inria.fr/seminars/170302.html). The
manual is still incomplete.