Project Filelist for CoqFiniteGroups

While the .v files are the ones part of 1.3pl1, the Coq plugin received many
fixes and is fully compatible with the .v files that will be released as part
of Ssreflect 1.4.

Changes:

- Views in intro patterns work even if alternated with regular intro
  patterns, like in "case=> a /v b".
- "set (f:= fun  _:Set =>0)" does not discard the anonymous abstraction
  anymore.
- "elim" correctly handles delta expansions and let-ins in the
  eliminator's type.
- "elim"'s predicate is typechecked to avoid generating an ill-typed
  goal.
- Different error messages for "dependent rewrite" errors and "indetermined
  RHS/LHS" errors.
- Nice error message for the illegal rewrite pattern "[X in t]" where "X"
  does not occur in "t".
- "apply: n." doesn't (try to) clear "n" if "n" is a section variable.
- Correctly handle (implicit) binders in have, suff and wlog tactics, like
  in "have f x : x \in [:: x]" where an extra binder is introduced for
  the type of "x".
- "rewrite" progress check takes instantiated evars into account.
- 'of' and '&' can be used in ssrbinders like in "have f of seq nat :...".
- "move=> a b" now performs weak-head beta-reduction before introducing
  "b".
- Interpret names after the "in" tactical with the right, Ltac-aware,
  function.