Ltac variable H is bound to OrderedType.EQ of type constr which cannot

Running command /usr/bin/python3 /github/workspace/coq-tools/find-bug.py -y /github/workspace/builds/coq/coq-failing/_build_ci/compcert/backend/Unusedglobproof.v /github/workspace/cwd/bug_01.v /github/workspace/cwd/tmp.v --error-log=/github/workspace/build.log --temp-file-log=/github/workspace/cwd/tmp.log --no-deps --ignore-coq-prog-args --inline-user-contrib --coqc=/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig --coqtop=/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqtop.orig --coq_makefile=/github/workspace/builds/coq/coq-passing/_install_ci/bin/coq_makefile --coqdep /github/workspace/builds/coq/coq-passing/_install_ci/bin/coqdep --base-dir=/github/workspace/builds/coq/coq-failing/_build_ci/compcert --ocamlpath=/github/workspace/builds/coq/coq-failing/_install_ci/lib: -Q /github/workspace/cwd Top --verbose-include-failure-warning --verbose-include-failure-warning-prefix ::warning:: --verbose-include-failure-warning-newline %0A --nonpassing-arg=-q --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/compcert/lib compcert.lib --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/compcert/common compcert.common --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/compcert/x86_32 compcert.x86_32 --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/compcert/x86 compcert.x86 --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/compcert/backend compcert.backend --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/compcert/cfrontend compcert.cfrontend --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/compcert/driver compcert.driver --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/compcert/cparser compcert.cparser --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/compcert/export compcert.export --nonpassing-arg=-native-compiler --nonpassing-arg=no --nonpassing-arg=-w --nonpassing-arg=-undeclared-scope --nonpassing-arg=-w --nonpassing-arg=-omega-is-deprecated --nonpassing-arg=-coqlib --nonpassing-arg=/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq// --passing-coqc=/github/workspace/builds/coq/coq-passing/_install_ci/bin/coqc.orig --passing-coqtop=/github/workspace/builds/coq/coq-passing/_install_ci/bin/coqtop.orig --passing-base-dir=/github/workspace/builds/coq/coq-failing/_build_ci/compcert --passing-ocamlpath=/github/workspace/builds/coq/coq-passing/_install_ci/lib: --passing-arg=-q --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/compcert/lib compcert.lib --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/compcert/common compcert.common --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/compcert/x86_32 compcert.x86_32 --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/compcert/x86 compcert.x86 --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/compcert/backend compcert.backend --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/compcert/cfrontend compcert.cfrontend --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/compcert/driver compcert.driver --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/compcert/cparser compcert.cparser --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/compcert/export compcert.export --passing-arg=-native-compiler --passing-arg=no --passing-arg=-w --passing-arg=-undeclared-scope --passing-arg=-w --passing-arg=-omega-is-deprecated --passing-arg=-coqlib --passing-arg=/github/workspace/builds/coq/coq-passing/_install_ci/lib/coq// -l - /github/workspace/bug.log --verbose-log-file 9999\,/github/workspace/bug.verbose.log

(/github/workspace/builds/coq/coq-passing) setting up coq_environment.txt: COQLIB="/github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/" COQCORELIB="/github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/../rocq-runtime/" DOCDIR="/github/workspace/builds/coq/coq-passing/_install_ci/share/doc/" OCAMLFIND="/root/.opamcache/4.14.2+flambda/bin/ocamlfind" CAMLFLAGS="-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70" WARN="-warn-error +a-3" HASNATDYNLINK="true" COQ_SRC_SUBDIRS="boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/ltac2_ltac1 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax" COQ_NATIVE_COMPILER_DEFAULT="yes"

(/github/workspace/builds/coq/coq-passing) /builds/coq/coq/_install_ci/bin/coqc --config: COQLIB=/github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/ COQCORELIB=/github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/../rocq-runtime/ DOCDIR=/github/workspace/builds/coq/coq-passing/_install_ci/share/doc/ OCAMLFIND=/root/.opamcache/4.14.2+flambda/bin/ocamlfind CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 WARN=-warn-error +a-3 HASNATDYNLINK=true COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/ltac2_ltac1 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax COQ_NATIVE_COMPILER_DEFAULT=yes

(/github/workspace/builds/coq/coq-failing) setting up coq_environment.txt: COQLIB="/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/" COQCORELIB="/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/../rocq-runtime/" DOCDIR="/github/workspace/builds/coq/coq-failing/_install_ci/share/doc/" OCAMLFIND="/root/.opamcache/4.14.2+flambda/bin/ocamlfind" CAMLFLAGS="-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70" WARN="-warn-error +a-3" HASNATDYNLINK="true" COQ_SRC_SUBDIRS="boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/ltac2_ltac1 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax" COQ_NATIVE_COMPILER_DEFAULT="yes"

(/github/workspace/builds/coq/coq-failing) /builds/coq/coq/_install_ci/bin/coqc --config: COQLIB=/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/ COQCORELIB=/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/../rocq-runtime/ DOCDIR=/github/workspace/builds/coq/coq-failing/_install_ci/share/doc/ OCAMLFIND=/root/.opamcache/4.14.2+flambda/bin/ocamlfind CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 WARN=-warn-error +a-3 HASNATDYNLINK=true COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/ltac2_ltac1 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax COQ_NATIVE_COMPILER_DEFAULT=yes

download passing artifacts @ f38be3de9b3898dab98af1185dfe2d5631e8a4e6 https://gitlab.inria.fr/coq/coq/-/jobs/5795122/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/5795053/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/5795081/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/5795083/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/5795089/artifacts/download

download failing artifacts @ 70315357bbb9962de852ffc83ca9ae70d52a609c https://gitlab.inria.fr/coq/coq/-/jobs/5797029/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/5796960/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/5796988/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/5796990/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/5796996/artifacts/download

ocamlfind ocamlopt -v: The OCaml native-code compiler, version 4.14.2 Standard library directory: /root/.opamcache/4.14.2+flambda/lib/ocaml

which ocamlfind: '/root/.opamcache/4.14.2+flambda/bin/ocamlfind'