Universe inconsistency. Cannot enforce j < i because i < j.

Using opam switch '4.09.0'

which ocamlfind: '/root/.opamcache/4.09.0/bin/ocamlfind'

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

download failing artifacts @ dc8315dd482007f5084bee93e95339388f69ff30 https://gitlab.inria.fr/coq/coq/-/jobs/4746792/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/4746875/artifacts/download

download passing artifacts @ 48db2360c32d779f948e110fdfbaae3d99c03fa3 https://gitlab.inria.fr/coq/coq/-/jobs/4740686/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/4740769/artifacts/download

/github/workspace/builds/coq/coq-failing/_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/../coq-core/ DOCDIR=/builds/coq/coq/_install_ci/share/doc/ OCAMLFIND=/root/.opamcache/4.09.0/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/_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/../coq-core/ DOCDIR=/builds/coq/coq/_install_ci/share/doc/ OCAMLFIND=/root/.opamcache/4.09.0/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

Running command /usr/bin/python3 /github/workspace/coq-tools/find-bug.py -y /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite/univ.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/ -Q /github/workspace/cwd Top --verbose-include-failure-warning --verbose-include-failure-warning-prefix ::warning:: --verbose-include-failure-warning-newline --nonpassing-arg=-q --nonpassing-arg=-w --nonpassing-arg=-deprecated-native-compiler-option --nonpassing-arg=-native-compiler --nonpassing-arg=no --nonpassing-I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq --nonpassing-I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq --nonpassing-I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq --nonpassing-I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq --nonpassing-I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure-plugin/src --nonpassing-I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/src --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/utils/theories MetaCoq.Utils --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/common/theories MetaCoq.Common --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories MetaCoq.PCUIC --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories MetaCoq.PCUIC --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories MetaCoq.Template --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/theories MetaCoq.SafeCheckerPlugin --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-pcuic/theories MetaCoq.TemplatePCUIC --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories MetaCoq.Template --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker/theories MetaCoq.SafeChecker --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories MetaCoq.Template --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories MetaCoq.Template --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-pcuic/theories MetaCoq.TemplatePCUIC --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure/theories MetaCoq.Erasure --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/theories MetaCoq.SafeCheckerPlugin --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure-plugin/theories MetaCoq.ErasurePlugin --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite MetaCoq.TestSuite --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-passing/_build_ci/ --passing-arg=-q --passing-arg=-w --passing-arg=-deprecated-native-compiler-option --passing-arg=-native-compiler --passing-arg=no --passing-I /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq --passing-I /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq --passing-I /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq --passing-I /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq --passing-I /

::warning::Failed to inline MetaCoq.Template.TemplateMonad.Common via Include, stripping Requires and preserve the error. The alternate coqc (/github/workspace/builds/coq/coq-passing/_install_ci/bin/coqc.orig) was supposed to pass, but instead emitted an error. The new error was: File "/tmp/tmpxoph8_a2/MetaCoq/TestSuite/univ.v", line 6, characters 8-21: Warning: Coq.Init.Ltac has been replaced by Stdlib.Init.Ltac. [deprecated-dirpath-Coq,deprecated-since-8.21,deprecated,default] File "/tmp/tmpxoph8_a2/MetaCoq/TestSuite/univ.v", line 12, characters 7-20: Warning: Coq.Init.Ltac has been replaced by Stdlib.Init.Ltac. [deprecated-dirpath-Coq,deprecated-since-8.21,deprecated,default] File "/tmp/tmpxoph8_a2/MetaCoq/TestSuite/univ.v", line 28, characters 0-28: Warning: Library File Stdlib.Bool.Bvector is deprecated since 8.20. Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector. [deprecated-library-file-since-8.20,deprecated-since-8.20,deprecated-library-file,deprecated,default] File "/tmp/tmpxoph8_a2/MetaCoq/TestSuite/univ.v", line 510, characters 0-96: Error: Anomaly "Constant MetaCoq.Template.TemplateMonad.Common.my_projT2 does not appear in the environment." Please report at http://coq.inria.fr/bugs/. The file generating the error was: (* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/utils/theories" "MetaCoq.Utils" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/common/theories" "MetaCoq.Common" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories" "MetaCoq.PCUIC" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories" "MetaCoq.Template" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/theories" "MetaCoq.SafeCheckerPlugin" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-pcuic/theories" "MetaCoq.TemplatePCUIC" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker/theories" "MetaCoq.SafeChecker" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure/theories" "MetaCoq.Erasure" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure-plugin/theories" "MetaCoq.ErasurePlugin" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite" "MetaCoq.TestSuite" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Equations" "Equations" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure-plugin/src" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/src" "-top" "MetaCoq.TestSuite.univ") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 263 lines to 23 lines, then from 31 lines to 215 lines, then from 220 lines to 31 lines, then from 38 lines to 205 lines, then from 210 lines to 39 lines, then from 46 lines to 505 lines, then from 507 lines to 128 lines, then from 135 lines to 403 lines, then from 406 lines to 201 lines, then from 208 lines to 598 lines, then from 602 lines to 291 lines *) (* coqc version 8.21+alpha compiled with OCaml 4.09.0 coqtop version runner-cabngxqim-project-4504-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at 46ba544a35489) (46ba544a3548941baad94eca61e125f289c5aa39) Expected coqc runtime on this file: 1.610 sec *) Require Coq.Init.Ltac. Module Export AdmitTactic. Module Import LocalFalse. Inductive False : Prop := . End LocalFalse. Axiom proof_admitted : False. Import Coq.Init.Ltac. Tactic Notation "admit" := abstract case proof_admitted. End AdmitTactic. Require Ltac2.Init. Require MetaCoq.Utils.MCEquality. Require MetaCoq