remove deprecated commands whose deprecation was introduced in 1.9.0

[ybertot]

fixes #418

Motivation for this change

Removing lemmas that were declared deprecated two releases before.

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md
• [ ] added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

[gares]

@CohenCyril what do you think about the failure of finmap? I know we are close to integrate finmap in MC (1.12) but for MC 1.11 there seem not to be any working version. Do you want to make a release.

[ybertot]

Failure of the ci-fourcolour-dev job is due to computation taking more than 1 hour, but recompilation on a dedicated machine succeeded.

[gares]

Let me restart the job, since it usually takes 45 minutes

[gares]

@CohenCyril told me that he shall make a pass on finmap & co to remove the use of deprecated aliases.

@CohenCyril could you write here what to do with this PR? Are you planning to update finmap soonish?

[ybertot]

@CohenCyril For your information, I tried testing quickly with the following process to replace the offending lemmas, but this does not compile, apparently for a reason independent from the change in this PR.

git clone git@github.com:math-comp/finmap.git
cd finmap
for i in $(find . -name '*.v') ; do perl -npi.bak -e 's/eq_big_perm/permP/;' \
 -e 's/perm_eq_mem/perm_mem/; s/perm_eqP/permP/; s/perm_eq_size/perm_size/;' \
 -e 's/perm_eq_small/perm_small_eq/; s/perm_eq_sym/perm_sym/;' \
 -e 's/perm_eq_trans/perm_trans/; s/perm_eq_uniq/perm_uniq/;' \
 -e 's/uniq_perm_eq/uniq_perm/' $i ; done

The offending line is at 2277 in finmap.v

[CohenCyril]

The culprit is

s/eq_big_perm/permP/

which should be s/eq_big_perm/perm_big/

[CohenCyril]

@CohenCyril told me that he shall make a pass on finmap & co to remove the use of deprecated aliases.

@CohenCyril could you write here what to do with this PR? Are you planning to update finmap soonish?

done, all lights are green now