Update the ssr examples

[co-dan]

Let me know what you think about these changes, Ralf.

[RalfJung]

I don't understand any of this code so I don't really have an opinion.^^ So, seems fine to me.

However, before landing:

• The README should be adjusted to remove the mention of ssreflect
• We should put the example on CI to make sure this actually works on all supported Coq examples. This will be easy once fix Coq 8.10 warnings and build examples on CI #16 lands and you rebase your PR on top of that.

[palmskog]

@co-dan @RalfJung this PR is a bit sad to me to read since the main task it accomplishes is to "de-depend" on coq-mathcomp-ssreflect. What is the main reason for removing this optional dependency? Recall that we can easily set up an opam file for the ssreflect examples which uses the right dependency at very little cost in CI.

Moreover, most SSReflect users in fact prefer to use the notations and definitions from coq-mathcomp-ssreflect rather than those in the Stdlib, so in my view the examples become less useful with this PR rather than more.

[co-dan]

@palmskog maybe it is better to make the old code work with the newer versions of ssreflect,
but I am not sure how to do this, due to the conflict between notations from mathcomp-ssreflect and autosubst

Moreover, most SSReflect users in fact prefer to use the notations and definitions from coq-mathcomp-ssreflect rather than those in the Stdlib, so in my view the examples become less useful with this PR rather than more.

you mean like using seq instead of list and so on?

[palmskog]

you mean like using seq instead of list and so on?

Yes, like +1 for successors. In some cases, the new notations do not map to Stdlib concepts, so the semantics may change when notations are changed.

[RalfJung]

Closing in favor of #20.