Make work with recent versions of Coq

[robbertkrebbers]

I tried to compile and run the development with Coq 8.17 and get some errors and warnings.

The errors are about Global being missing, I will open a pull request for that.

The warnings are as follows:

Ignored instance declaration for “sym”: “forall (A : Type)
                                           (cmp : A -> A -> comparison),
                                         SymTrans cmp -> Sym cmp” is not a class

Ignored instance declaration for “tra”: “forall (A : Type)
                                           (cmp : A -> A -> comparison),
                                         SymTrans cmp -> Trans cmp” is not a class

"auto with *" was used through the default "intuition_solver" tactic.