Add an is_cofix tactic

Should we also add is_* tactics for other things?  is_rel, is_meta,
is_sort, is_cast, is_prod, is_lambda, is_letin, is_app, is_const,
is_ind, is_constructor, is_case, is_proj?
Fixing the essence of naming bug #3204: use same strategy for naming
cases pattern variables than for naming forall/fun binders (but still
avoiding constructor names).

Note in passing: such as it is implemented, the general strategy is in
O(n²) in the number of nested binders, because, when computing the
name for each 'fun x => c" (or forall, or a pattern name), the names
from the outside c and visibly occurring in c are computed.
Fix computation of dangling constraints at the end of a proof (bug #3531).
Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible
to match on a primitive projection application c.(p) using "?f _", binding f
to (fun x => x.(p)) with the correct typing.
Fix compilation error due to commented code in previous commit by Hugo.
Make evarconv and unification able to handle eta for records in presence
of metas/evars
Do not pass "-batch" or "-load-vernac-source" to slaves, avoiding errors in
stm test-suite files.
Generalize EqdepFacts

The generalized versions are names *_one_var.  We preserve backwards
compatibility by defining the old versions in terms of the generalized
ones.

This closes the rest of Bug 3019, and closes pull request #6.
sed s'/_one_var/_on/g'

For consistency with ChoiceFacts