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.