Some unresolved existential variables remain

Some unresolved existential variables remain

Using opam switch '4.14.1+flambda'

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

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

download failing artifacts @ cecd17315cceead371ebd704ec97df139dad33e8 https://gitlab.com/coq/coq/-/jobs/4437684128/artifacts/download https://gitlab.com/coq/coq/-/jobs/4437684172/artifacts/download

download passing artifacts @ 6e739ce1f8ec685f7e409f0799a894c45c4325ea https://gitlab.com/coq/coq/-/jobs/4436252752/artifacts/download https://gitlab.com/coq/coq/-/jobs/4436253439/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.14.1+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/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.14.1+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/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/cwd/bug_01.v /github/workspace/cwd/bug_01.v /github/workspace/cwd/tmp.v --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=+implicit-core-hint-db\,+implicits-in-term\,+non-reversible-notation\,+deprecated-intros-until-0\,+deprecated-focus\,+unused-intro-pattern\,+variable-collision\,+unexpected-implicit-declaration\,+omega-is-deprecated\,+deprecated-instantiate-syntax\,+non-recursive\,+undeclared-scope\,+deprecated-hint-rewrite-without-locality\,+deprecated-hint-without-locality\,+deprecated-instance-without-locality\,+deprecated-typeclasses-transparency-without-locality\,unsupported-attributes --nonpassing-arg=-w --nonpassing-arg=-notation-overridden\,-deprecated-hint-constr\,-fragile-hint-constr\,-native-compiler-disabled\,-ambiguous-paths\,-masking-absolute-name --nonpassing-arg=-w --nonpassing-arg=-deprecated-native-compiler-option --nonpassing-arg=-native-compiler --nonpassing-arg=ondemand --nonpassing-Q /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src/coqutil coqutil --nonpassing-Q /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/src/Rupicola Rupicola --nonpassing-Q /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2 bedrock2 --nonpassing-Q /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples bedrock2Examples --nonpassing-Q /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler compiler --nonpassing-Q /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv riscv --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src Crypto --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=+implicit-core-hint-db\,+implicits-in-term\,+non-reversible-notation\,+deprecated-intros-until-0\,+deprecated-focus\,+unused-intro-pattern\,+variable-collision\,+unexpected-implicit-declaration\,+omega-is-deprecated\,+deprecated-instantiate-syntax\,+non-recursive\,+undeclared-scope\,+deprecated-hint-rewrite-without-locality\,+deprecated-hint-without-locality\,+deprecated-instance-without-locality\,+deprecated-typeclasses-transparency-without-locality\,unsupported-attributes --passing-arg=-w --passing-arg=-notation-overridden\,-deprecated-hint-constr\,-fragile-hint-constr\,-native-compiler-disabled\,-ambiguous-paths\,-masking-absolute-name --passing-arg=-w --passing-arg=-deprecated-native-compiler-option --passing-arg=-native-compiler --passing-arg=ondemand --passing-Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src/coqutil coqutil --passing-Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/src/Rupicola Rupicola --passing-Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2 bedrock2 --passing-Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples bedrock2Examples --passing-Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/compil

::warning::Failed to inline Rewriter.Util.plugins.RewriterBuildRegistry via Include, stripping Requires and preserve the error. The new error was: File "/tmp/tmpplojhcic/Top/bug_01.v", line 283, characters 0-9: Warning: Let definition cast_outside_of_range declared as an axiom. [let-as-axiom,vernacular,default] File "/tmp/tmpplojhcic/Top/bug_01.v", line 494, characters 2-230: Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. The file generating the error was: (* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+undeclared-scope,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+deprecated-typeclasses-transparency-without-locality,unsupported-attributes" "-w" "-notation-overridden,-deprecated-hint-constr,-fragile-hint-constr,-native-compiler-disabled,-ambiguous-paths,-masking-absolute-name" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src" "Crypto" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/src/Rupicola" "Rupicola" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2" "bedrock2" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples" "bedrock2Examples" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler" "compiler" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv" "riscv" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Coqprime" "Coqprime" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Rewriter" "Rewriter" "-top" "Top.bug_01") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 1498 lines to 11 lines, then from 24 lines to 324 lines, then from 329 lines to 52 lines, then from 65 lines to 384 lines, then from 389 lines to 57 lines, then from 70 lines to 840 lines, then from 845 lines to 118 lines, then from 131 lines to 380 lines, then from 385 lines to 130 lines, then from 143 lines to 339 lines, then from 344 lines to 132 lines, then from 150 lines to 132 lines, then from 145 lines to 478 lines, then from 484 lines to 255 lines, then from 269 lines to 501 lines, then from 506 lines to 351 lines, then from 365 lines to 694 lines, then from 699 lines to 825 lines, then from 833 lines to 357 lines, then from 370 lines to 564 lines, then from 570 lines to 377 lines, then from 391 lines to 987 lines, then from 992 lines to 377 lines, then from 391 lines to 3948 lines, then from 3948 lines to 4401 lines, then from 4405 lines to 389 lines *) (* coqc version 8.18+alpha compiled with OCaml 4.14.1 coqtop version runner-vxtc-u6t-project-6138686-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at d7ce6d9) (d7ce6d9deac92848bd8420d857a18a96a87da88b) Expected coqc runtime on this file: 7.769 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 Crypto.Util.Tactics.SubstEvars. Require Crypto.Util.ListUtil.Filter. Require Crypto.Util.ZUtil.Definitions. Import Coq.Li