Add coq.univ.alg-super, @keep-alg-univs!

[lweqx]

This is #585 rebased on master.

This should close both #585 and #400.

[gares]

Thanks!!

[CohenCyril]

Are the docker CI expected to fail?

[CohenCyril]

Before merging I would just like a constructive proof that this is enough to port Trocq to modern Coq/Rocq versions ;)
CC @lweqx (do not hesitate to ping me if you require my help)

[lweqx]

Are the docker CI expected to fail?

I think the failures originate from a warning being treated as an error in tests/test_HOAS.v :

2025-04-18T15:35:23.8389557Z Error:
2025-04-18T15:35:23.8389875Z File "./tests/test_HOAS.v", line 663, characters 2-58
2025-04-18T15:35:23.8390446Z The standard λProlog infix operator for implication => has higher precedence
2025-04-18T15:35:23.8390769Z than conjunction. This means that 'A => B, C' reads '(A => B), C'.
2025-04-18T15:35:23.8391146Z This is a common mistake since it makes A only available to B (and not to C
2025-04-18T15:35:23.8391357Z as many newcomers may expect).
2025-04-18T15:35:23.8391773Z If this is really what you want write '(A => B), C' to silence this warning.
2025-04-18T15:35:23.8392146Z Otherwise write 'A => (B, C)', or use the alternative implication operator ==>.
2025-04-18T15:35:23.8392455Z Infix ==> has lower precedence than conjunction, hence
2025-04-18T15:35:23.8392712Z 'A ==> B, C' reads 'A ==> (B, C)' and means the same as 'A => (B, C)'.
2025-04-18T15:35:23.8392975Z [elpi.implication-precedence,elpi,default]

This should be easy to fix.

[gares]

Even if not enough, this change is OK on my side. I would not let it bitrot

[CohenCyril]

alright, then merge first and check Trocq later on