Support coq-mathcomp-field >= 2.0

[erikmd]

No description provided.

[erikmd]

Hi @proux01, FYI:

• I fixed the opam issue (extra-dev was temporarily needed)

• Now it seems the proof goes beyond the previous attempt, but the CI still fails.

IIUC (just skimmed the log), validsdp.v compiles But testsuite.v doesn't:

  - for f in test-suite/matrices.v test-suite/testsuite.v test-suite/test_validsdp.v test-suite/test_validsdp_intro.v ; do \
  -   "/home/coq/.opam/4.13.1+flambda/bin///coqc"  -q '-w' '-notation-overridden' '-w' '-ambiguous-paths'  "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I plugins/soswitness/src  -R plugins/soswitness/theories ValidSDP -R plugins/soswitness/src ValidSDP -R plugins/soswitness/test-suite ValidSDP -R test-suite ValidSDP -R theories ValidSDP $f ; \
  - done
  - File "./test-suite/testsuite.v", line 2, characters 0-51:
  Error: - Error: Universe inconsistency. Cannot enforce prod.u0 <=
  - hrel.hrespectful.u0 because hrel.hrespectful.u0 <= eqtype.isSub.axioms_.u1
  - < eqtype.isSub.axioms_.u0 <= eqtype.isSub.phant_axioms.u2 <= prod.u0.
  - 
  - File "./test-suite/test_validsdp.v", line 2, characters 0-51:
  Error: - Error: Universe inconsistency. Cannot enforce prod.u0 <=
  - hrel.hrespectful.u0 because hrel.hrespectful.u0 <= eqtype.isSub.axioms_.u1
  - < eqtype.isSub.axioms_.u0 <= eqtype.isSub.phant_axioms.u2 <= prod.u0.
  - 
  - File "./test-suite/test_validsdp_intro.v", line 2, characters 0-51:
  Error: - Error: Universe inconsistency. Cannot enforce prod.u0 <=
  - hrel.hrespectful.u0 because hrel.hrespectful.u0 <= eqtype.isSub.axioms_.u1
  - < eqtype.isSub.axioms_.u0 <= eqtype.isSub.phant_axioms.u2 <= prod.u0.
  - 
  - make[1]: *** [Makefile.coq.local:34: test] Error 1   # hrel.hrespectful.u0 because hrel.hrespectful.u0 <= eqtype.isSub.axioms_.u1

[proux01]

Fixed