# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq 8.16.0 Formal proof management system
dune 3.7.0 Fast, portable, and opinionated build system
ocaml 4.11.2 The OCaml compiler (virtual package)
ocaml-base-compiler 4.11.2 Official release 4.11.2
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.5 A library manager for OCaml
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "forster@cs.uni-saarland.de"
homepage: "https://github.com/uds-psl/coq-library-undecidability/"
dev-repo: "git+https://github.com/uds-psl/coq-library-undecidability/"
bug-reports: "https://github.com/uds-psl/coq-library-undecidability/issues"
authors: ["Yannick Forster"
"Dominique Larchey-Wendling"
"Andrej Dudenhefner"
"Edith Heiter"
"Marc Hermes"
"Johannes Hostert"
"Dominik Kirst"
"Mark Koch"
"Fabian Kunze"
"Gert Smolka"
"Simon Spies"
"Dominik Wehr"
"Maximilian Wuttke"]
license: "CECILL-2.1"
build: [
[make "-j%{jobs}%"]
]
install: [
[make "install"]
]
depends: [
"coq" {>= "8.16.0" & < "8.17"}
"ocaml"
"coq-smpl" {>= "8.16"}
"coq-metacoq-template" {>= "1.1+8.16"}
]
synopsis: "A Coq Library of Undecidability Proofs"
url {
src: "https://github.com/uds-psl/coq-library-undecidability/archive/v1.0.1+8.16.tar.gz"
checksum: "sha256=96febb4482b41810782dca089144b1bffcb91ab1975dc9e312efacf3bf2e4371"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-library-undecidability.1.0.1+8.16 coq.8.16.0Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-library-undecidability.1.0.1+8.16 coq.8.16.0opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-library-undecidability.1.0.1+8.16 coq.8.16.0Total: 131 M
../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/HeapInterpreter/StepTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_eqb.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_basics.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB/CM1_to_SMX.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_minZF.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_rem_cst.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Matija/cipher.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/PCPb_to_HaltL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Single/StepTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_binZF.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB/CM1_to_SMX.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_minZF.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/Arbitrary_to_Binary.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/Util/PA2_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/HeapInterpreter/JumpTargetTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/TM_computable_to_BSM_computable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_elem.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/BPCP_SigBPCP.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FSAT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/MM2_ZERO_HALTING_to_SSTS01.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_utils.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/Compare.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/HeapInterpreter/UnfoldClos.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/pure_typable_prenex.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/Compiler.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_utils.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_no_self.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Reductions/H10C_SAT_to_SysF_INH.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/HeapInterpreter/M_LHeapInterpreter.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/MuRec/MuRec_extract.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_utils.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/NatTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_utils.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_mm_env.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LNat.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/TM_computable_to_BSM_computable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/MM2_ZERO_HALTING_to_SSTS01.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_univ_andrej.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosCompareTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_fold.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Single/StepTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/TM/TapeFuns.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_utils.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_binZF.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Matija/alpha.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CaseList.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Matija/cipher.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/Transcode/Boollist_to_Enc.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/AbstractMachines/FlatPro/LM_heap_correct.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/KOSBTM/HaltKOSBTM_to_HaltBSM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_REV_HALT_dec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/HaltMuRec_to_HaltL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Reductions/PCPb_to_FOLFS.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_UBOUNDED_dec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_pcp.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL_minimal.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/gcd.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/SMN_transform.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosAddTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/H10_to_L.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FSAT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Autosubst/syntax.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/bool_nat.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/FOL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Reductions/H10C_SAT_to_SysF_INH.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/firstorder.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_computable_to_MM_computable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Decoding.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/NTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Reflection.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/CopySymbols.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/KOSBTM/HaltKOSBTM_to_HaltBSM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/HeapInterpreter/StepTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareRegister.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/bool_nat.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/LinDecode/LTDlist.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/MoveToSymbol.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_computable_to_MM_computable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_mm_env.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/HeapInterpreter/LookupTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/KrivineMclosed_HALT_to_HaltUTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/KrivineMclosed_HALT_to_MMA_HALTING.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Matija/alpha.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_ca.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/Copy.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/SMN_transform.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SetConstraints/Reductions/H10UC_SAT_to_FMsetC_SAT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMenv/mme_utils.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_bounded.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/schellinx.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/ArithLibs/Zp.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosShiftTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CasePair.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL_minimal.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/AbstractMachines/FlatPro/LM_heap_def.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_single.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/H10Z_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_utils.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/List/Length.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/CSSM_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/List/Rev.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_nat.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_ZFD.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/Transcode/Enc_to_Boollist.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LVector.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_ZF.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosMultTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/ResourceMeasures.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/KOSBTM/HaltTM_1_to_HaltKOSBTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/KrivineMclosed_HALT_to_MMA_HALTING.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_REV_HALT_dec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/pure_typing_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MPM2_HALT_dec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_dio_poly.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/TM/TMEncoding.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_UBOUNDED_dec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_list.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/List/Nth.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/EncBoolsTM_boolList.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/Eval.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/ArithLibs/lagrange.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/sss.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/ArithLibs/luca.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HilbertCalculi/Reductions/MPCPb_to_HSC_PRV.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/Util/Subst.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/TM/TMinL/TMinL_extract.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/List/App.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL_full_fragment.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/pure_typable_prenex.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/ArithLibs/Zp.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/TM_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/btree.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Reductions/PCPb_to_FOLFS.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/Copy.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Util/L_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/sorting.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Encoding.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_Sig_fin.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/firstorder.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CaseSum.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SetConstraints/Reductions/H10UC_SAT_to_FMsetC_SAT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/Util/Tarski.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CounterMachines/Reductions/MM2_HALTING_to_CM1_HALT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/Util/Syntax.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/Arbitrary_to_Binary.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/Shift.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/pure_typing_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_logic.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_extra.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareRegister.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/reln_hfs.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/HaltTM_1_to_SBTM_HALT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Syntax_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_ZF.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/Code.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SeparationLogic/Reductions/FSATdc_to_MSLSAT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/terms_extension.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LOptions.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareMult.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/Compiler_nat_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Synthetic.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/unification/enumerability.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/ComputableDemo.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/gcd.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareCombinators.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CaseList.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/FinTypeLookup.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/btree.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Equality.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Vec/vec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/Compiler_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_nat.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_ZFD.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN/mm_fractran.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_utils.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/List/Concat_Repeat.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/CSSM_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/sss.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_logic.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/FullFOL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_univ.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_cipher.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/FOL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/eill_mm.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Extract.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_list.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Seval.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LTerm.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/encoding.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CompareValue.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/discrete.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Subst.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_in.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MPM2_HALT_dec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/LinDecode/LTDnat.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/HaltTM_1_to_SBTM_HALT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/SBTM_HALT_to_HaltBSM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Vec/vec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/ArithLibs/lagrange.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/multiplication.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_binary.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/prime.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/dowek/encoding.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM_2_HALTING_dec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LSum.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_congruence.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_utils.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/Compiler.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/third_order/encoding.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/reduction.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Prelim/ARS.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_discernable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LProd.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/ComputableTactics.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/ComputableTime.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_rem_syms.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL_full_fragment.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Autosubst/syntax.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/HeapInterpreter/UnfoldClos.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/HeapInterpreter/JumpTargetTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CounterMachines/Reductions/MM2_HALTING_to_CM1_HALT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/SBTM_HALT_to_HaltBSM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/TM_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/poly_type_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareLogic.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/Compare.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosHelperMachines.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig2_SigSSn1.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/sums.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/SBTM_HALT_to_SR.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareCombinators.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Size.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/NatSub.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Deciders/Halt_REV_FRACTRAN_dec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Proc.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Eval.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/fractran_mma.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Matija/expo_diophantine.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/AbstractMachines/FlatPro/LM_heap_correct.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/terms_extension.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/sums.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/concon/constants.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HilbertCalculi/Reductions/MPCPb_to_HSC_PRV.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/recomp.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/membership.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/LoopSum.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/third_order/huet.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/ArithLibs/luca.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_logic.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_ZFeq.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA2_to_ndMM2_ACCEPT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/CSSM_UB_to_SSemiU.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/HaltMuRec_to_HaltL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/enumerable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/BPCP_SigBPCP.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/encoding.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/fractran_mma.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_mm.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/concon/enumerability.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/concon/constants.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/Util/Syntax.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/step.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/DoubleNegation.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/Util/Subst.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/SBTM_HALT_to_HaltTM_1.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_expo.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_utils_bsm.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/power_decomp.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SeparationLogic/Reductions/FSATdc_to_MSLSAT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Syntax_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/NatTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_REV_dec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/LClos_Eval.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Util/H10UPC_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/discrete.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Lifting/LiftTapes.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/CSSM_UB_to_SSemiU.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/Util/PA2_categoricity.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/SMN_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/concon/conservativity.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/php.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/ClosedLAdmissible.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_logic.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Reductions/HaltLclosed_to_wCBNclosed.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/Util/PA2_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MM2_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/bool_list.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/StateWhile.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig1_1.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_no_self.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN/fractran_utils.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_Sig_fin.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/membership.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HilbertCalculi/Reductions/MPCPb_to_HSC_AX.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/compiler_correction.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Lrewrite.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareLogic.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CodeTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/FinNotation.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/FullDeduction_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/SBTM_HALT_to_SR.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CaseCom.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/ChangeAlphabet.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN/mm_fractran.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/bool_list.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Reductions/LU2SemiU_to_SysF_TYP.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosShiftTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Util/prime_seq.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Single/StepTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMenv/mme_utils.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/semantics.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/hfs.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/MMA_HALTING_n_to_HaltTM_n.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_elem.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosAddTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/rel_iter.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/LinDecode/LTDbool.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/Util/PA2_categoricity.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_defs.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/UnboundIteration.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/SBTM_HALT_to_TSR.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Single/EncodeTapes.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/MoveToSymbol.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/enumerable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_pctm.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/PCTM/pctm_sbtm.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/concon/conservativity_constants.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/reduction.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_minZFeq.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_nat.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/ArithLibs/matrix.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CaseNat.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/LClos.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_ZFeq.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/typing_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/HeapInterpreter/M_LHeapInterpreter.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/poly_type_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB/CM1_to_SMX.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/Vectors.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/concon/conservativity.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Util/L_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_enum.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Retracts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/MPCP_to_PCP.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_utils_bsm.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/order.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/Reductions/CFPP_to_CFP.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Vec/pos.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/Transcode/Boollist_to_Enc.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_pctm.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/compiler_correction.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/sn_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_sat_dec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/unification/systemunification.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_defs.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Lifting/LiftTapes.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Reductions/LU2SemiU_to_SysF_TYP.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/crt.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/recalg.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/SBTM_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/MuRec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/unification/nth_order_unification.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Reductions/ndMM2_IMSELL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/FullDeduction_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/AbstractMachines/FlatPro/Programs.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LBool.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/Switch.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/hfs.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/sorting.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_univ_andrej.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMenv/mme_defs.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Extract.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/lists/advanced.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MM2_to_ndMM2_ACCEPT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_definable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_recomp.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/StateWhile.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/equivalence.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/HeapInterpreter/LookupTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_rem_constants.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/Code.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/lists/basics.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/subcode.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosIncrementTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Util/Definitions.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_defs.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MM_sss.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/EqBool.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/EncBoolsTM_boolList.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_single.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/unification/enumerability.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FOL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_decidable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/compiler.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/BSM_sss.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/H10SQC_SAT_to_H10UC_SAT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/FullTarski_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_k_mma_2_compiler.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Computable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Reflection.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_terms.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_discernable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Lifting/LiftAlphabet.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CasePair.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Reductions/ndMM2_IMSELL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/Util/Tarski.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/While.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/AbstractMachines/FlatPro/UnfoldClos.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig1_1.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/FullFOL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/unification/nth_order_unification.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/enumerable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/list_bool.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Por.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_defs.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_base.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LFinType.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/decidable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/Lists.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/While.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_comp_strong.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_univ.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/DPRM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/recalg.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/multiplication.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_quotient.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/quotient.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CounterMachines/Util/CM1_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_enc.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/Models_Equivalent.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/syntax.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/red_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Reductions/HaltLclosed_to_wCBNclosed.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/Multi.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Acceptability.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_rem_syms.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM_2_HALTING_dec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/ListEnumerabilityFacts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sign1_Sig.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/List/Nth.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/godel_coding.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/List/Cons_constant.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareMult.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_one_rel.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/third_order/encoding.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Prelim/ARS.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Kripke.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/ResourceMeasures.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/dowek/encoding.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/seteq.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/PCTM/pctm_sbtm.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/ill.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/eill_mm.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/Reductions/PCP_to_CFPI.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/PrettyBounds/MaxList.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_congruence.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Util/Facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sign_Sig2.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_minZFeq.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/enumerable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/GenEncode.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA2_to_MM2.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosCompareTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/FA_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FOL_class.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Ackermann.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Deduction.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/concon/enumerability.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/KOSBTM/HaltKOSBTM_to_HaltKOSBTMu.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/Compiler_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/FRACTRAN_to_H10C_SAT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosPointers.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FOL_class.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/EqDec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/UpToC.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/ZF_model.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/Transcode/BoollistEnc.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/bpcp.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/php.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Deciders/Halt_REV_FRACTRAN_dec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareTactics.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/TM_computable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/terms.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Lbeta.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/L_to_mTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/reln_hfs.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HilbertCalculi/Reductions/MPCPb_to_HSC_AX.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Autosubst/syntax.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CaseSum.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/Reductions/H10p_to_SOL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_comp_strong.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/FA_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/term_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/prelim.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/typing_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/SMNdl_UB_to_CSSM_UB.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/imsell.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/CLL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Lists/BaseLists.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/UpToCNary.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/FullSyntax.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_dio_poly.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/CopySymbols.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_bounded.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/Compiler_nat_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/mTM_to_TM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/ars/basic.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CaseFin.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/sn_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_comp.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_uniform.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Matija/cipher.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/eill.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10p_to_FA.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/Combinators.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_defs.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CaseBool.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/third_order/simplified.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/List/App.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Util/prime_seq.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/third_order/huet.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/NaryApp.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Lsimpl.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/SR_to_MPCP.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/ars/list_reduction.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosHelperMachines.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_definable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosDefinitions.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_comp.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/EnumerabilityFacts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/FullSyntax.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/TM/TMinL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/ArithLibs/matrix.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/gfp.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/List/Length.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/Reductions/CFPP_to_CFP.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN/fractran_utils.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/eill.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Decidability.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMenv/mme_defs.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Prelim/MoreList.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/SSemiU_to_RU2SemiU.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/TRAKHTENBROT_to_FSAT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/Prelim.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/Alphabets.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/crt.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Util/H10UPC_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/FinTypes.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_UMORTAL_dec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Tarski.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB/SMX_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/CLL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/dowek/reduction.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/terms.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/WriteString.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/Shift.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/WriteValue.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FOL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_bij.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/TM_to_L.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/rel_iter.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/L_computable_to_TM_computable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/LComp_to_TMComp.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/Infinite.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Reductions/FRACTRAN_computable_to_Diophantine.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/TMTac.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/UTM_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/ClosedLAdmissible.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/ILL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CompareValue.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/List/Rev.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosMultTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/TM/TMinL/TMinL_extract.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/decidable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/prime.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/minFOL_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/seteq.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/ill_cll_restr.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/SMN_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/Syntax.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/EncodeBinNumbers.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/unification/systemunification.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_ca.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_utils.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Krivine_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/lists/advanced.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/Mirror.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Util/PCP_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_no_syms.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MM2_HALTING_to_MM2_ZERO_HALTING.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PolynomialConstraints/Reductions/FMsetC_SAT_to_LPolyNC_SAT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_k_mma_2_compiler.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/FullTarski.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/ChangeAlphabet.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/SysF_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/SOL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/wCBN_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/axioms.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/ILL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig2_SigSSn1.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/Compiler_spec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig0.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Vec/pos.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/H10_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_rem_props.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_upto.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Basic/Mono.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Util/Krivine_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/BSM_computable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/List_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig1.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/normalisation.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/decidable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/ListEnumerabilityFacts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/Transcode/Enc_to_Boollist.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_defs.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/MPCP_to_PCP.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/typing.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/L_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/NTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/iipc2_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA2_to_MM2.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Fractran/fractran_dio.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_terms.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/minZF_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/MMA_HALTING_n_to_HaltTM_n.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/AbstractMachines/LargestVar.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Seval.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/power_decomp.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/Reductions/H10p_to_SOL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/Relations.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_sat_dec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/Switch.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/IMSELL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CodeTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Lbeta_nonrefl.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Computability.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/H10SQC_SAT_to_H10UC_SAT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_mm.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sign_Sig2.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Reductions/H10C_SAT_to_SysF_INH.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Util/term_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FSAT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_enum.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/unscoped.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/order.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/H10C_SAT_to_H10SQC_SAT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/binomial.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/red_dec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/bool_nat.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_binZF.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/TM_computable_to_BSM_computable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/godel_coding.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/concon/conservativity_constants.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/Syntax.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/MuRec_computable_to_L_computable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/SR_to_PCSnf.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Reductions/MM_computable_to_FRACTRAN_computable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Reductions/Diophantine_to_MuRec_computable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/MuRec_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Lproc.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/H10C_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/ComputableTime.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/RA_UNIV_HALT_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareStdLib.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/AbstractMachines/FlatPro/LM_heap_def.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/minZF.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/PA_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/PA2_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/HaltTM_1_chain_SemiU.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/SOL_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/confluence.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/dowek/reduction.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/SemiU_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Aczel_TD.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCP_to_PCPb.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/lists/misc.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_minZF.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/ZF_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_simul.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Lrewrite.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/prim_min.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/subcode.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LUnit.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/bounded_quantification.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MM2_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/ZF.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Matija/alpha.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Aczel.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_godel_beta.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/LClos.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Aczel_TD.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PolynomialConstraints/LPolyNC_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/FSAT_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/H10p_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/Vectors.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/reductions.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/wf_chains.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/HaltL_to_HaltTM_5.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_mm_env.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SetConstraints/FMsetC_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Syntax.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/SSM_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Fixpoints.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/FullDeduction.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Reductions/HaltTM_1_to_SysF_TC.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/SMN_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Reductions/HaltTM_1_to_SysF_TYP.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_noeq.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/IMSELL_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/ill.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/HeapInterpreter/StepTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Synthetic.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sign_Sig.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SeparationLogic/SL_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/pure_typable_prenex.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/imsell.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/unification/higher_order_unification.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL_minimal.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/red_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/term_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_base.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/H10UC_SAT_to_H10UPC_SAT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SeparationLogic/MSL_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/MoreEnumerabilityFacts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/ILL_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/PrettyBounds/MaxList.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/Nat_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CounterMachines/CM1_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/SBTM_HALT_to_HaltTM_1.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Reductions/HaltTM_1_to_SysF_INH.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/ars/confluence.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/HaltTM_1_to_SemiU.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/ars/evaluator.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM2_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/HaltL_to_HaltLclosed.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/SSTS_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/If.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Aczel_CE.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/Facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/LinDecode/LTD_def.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/HaltTM_1_to_CSSM_UB.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/VectorForall.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/PCTM/pctm_defs.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/ndMM2_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/binFOL_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA2_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_REV_HALT_dec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fol_ops.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB/SMX_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Decoding.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HilbertCalculi/Util/HSCFacts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Aczel.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Dec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_rem_cst.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Aczel_CE.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA2_to_ndMM2_ACCEPT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/iPCPb_to_BSM_HALTING.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/binZF_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/CompoundFinTypes.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/CLL_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/EnumerabilityFacts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/lists/basics.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/minimizer.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareRegister.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CounterMachines/Reductions/HaltTM_1_to_CM1_HALT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/compiler.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/red_dec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/ill_cll.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/bsm_mma.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/VectorDupfree.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/SMN_transform.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Prelim/MoreBase.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/unscoped.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/PA.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_sem_eq.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/discernable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/third_order/pcp.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/firstorder.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_uniform.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/List/Concat_Repeat.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/ProgrammingTools.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_rt_closure.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_bij.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Prelim/LoopSum.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/Eval.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig2_Sign.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/FOL_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/motivation.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/HaltTM_1_to_PCPb.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/MM2_ZERO_HALTING_to_SSTS01.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/RU2SemiU_to_LU2SemiU.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/Arbitrary_to_Binary.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Util/Definitions.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/DecidabilityFacts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Reductions/HaltTM_1_to_FRACTRAN_HALTING.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Basic/Duo.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/countability.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/H10Z.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/H10_to_L.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/quotient.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/GenericNary.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Matija/expo_diophantine.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/binZF.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/ars/basic.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/HaltTM_1_to_MM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10p_to_FA.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/BSM_sss.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CounterMachines/Util/CM1_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Lifting/LiftAlphabet.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MM2_to_ndMM2_ACCEPT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/ArithLibs/Zp.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MM_sss.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/UTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/PCP_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_choice.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/minZF.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HilbertCalculi/HSC_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/CFG_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/mTM_to_TM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Util/FRACTRAN_computable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/ListAutomation.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/measure_ind.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/list_bool.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MM2_HALTING_to_MM2_ZERO_HALTING.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_recomp.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/TM_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/CFP_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/unscoped.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_binary.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Reductions/MM_FRACTRAN.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Util/wCBN_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/VectorFin.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma3_mma2_compiler.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/equivalence.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/RU2SemiU_to_LU2SemiU.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/HaltTM_1_to_iPCPb.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/AbstractMachines/FlatPro/Programs.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Util/Enumerable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/btree.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/Util/Facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/concon/constants_consequences.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/FinTypes.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/HaltTM_1_to_PCP.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/Copy.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPb_iff_iPCPb.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/TM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/wf_incl.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosDefinitions.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/LTactics.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/pure_typing_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/FRACTRAN_DIO.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/FullTarski_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/Reductions/PCP_to_CFPP.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/PCSnf_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/SR_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/BasicDefinitions.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/MoreReducibilityFacts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/SBTM_undec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_choice.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/SSemiU_to_RU2SemiU.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/interval.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/PrettyBounds/SizeBounds.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/DoubleNegation.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Reductions/H10_to_H10p.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/HaltTM_1_to_SR.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Reductions/MM_computable_to_FRACTRAN_computable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/SequentialComposition.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_computable_to_MM_computable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/SR_to_PCSnf.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Reductions/wCBNclosed_to_KrivineMclosed_HALT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_sig.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/ListTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/wf_finite.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/MuRec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_MM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Retracts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_simul.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/TM_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/evaluator.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_decidable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/DPRM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_sat.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MM_computable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/FRACTRAN_to_H10C_SAT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/ZF.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/FOL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_quotient.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Reductions/H10_to_MUREC_HALTING.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/FullTarski.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Computable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/pure_term_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/SBTM_HALT_to_TSR.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SeparationLogic/Reductions/MSLSAT_to_SLSAT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/utils.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/Prelim.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Basic/Mono.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PolynomialConstraints/Reductions/FMsetC_SAT_to_LPolyNC_SAT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/sss.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Autosubst/unscoped.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/KOSBTM/HaltTM_1_to_HaltKOSBTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_dec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/red_utils.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MUREC_MM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/UnboundIteration.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LVector.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_basics.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/DepPairs.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/syntax.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Util/h10c_utils.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_pcp.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Util/FRACTRAN_sss.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/semantics.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_discrete.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/UpToCNary.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Autosubst/unscoped.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/PA2.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/misc.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_tac.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/Infinite.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/decidable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/bpcp.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Lists/BaseLists.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/prelim.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/H10C_SAT_to_H10SQC_SAT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/SR_to_MPCP.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/ComputableTactics.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/SBTM_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/UpToC.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Deduction.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/KOSBTM/HaltKOSBTM_to_HaltBSM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/Hoare.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Inhabited.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/gfp.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/gcd.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/diophantine_equations.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FOL_intu.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/red_enum.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Single/EncodeTapes.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/GenEncode.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMenv/env.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/PCTM/pctm_defs.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/MPCP_to_MPCPb.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Enumerators/term_enum.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/retracts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM2.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/SOL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MM_to_MMA2.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_UBOUNDED_dec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/recursor.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/Util/Syntax.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/bounded_quantification.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPX_iff_dPCP.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/Enumerable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/H10Z_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/List_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/ArithPrelim.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/Relations.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/KrivineMclosed_HALT_to_MMA_HALTING.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Fractran/fractran_dio.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/ars/evaluator.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SeparationLogic/Reductions/MSLSAT_to_SLSAT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/PCTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/AbstractMachines/FlatPro/ProgramsDef.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_utils.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Reductions/H10C_SAT_to_RA_UNIV_HALT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_rem_constants.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Basic/Null.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareLegacy.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_simul.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_ZF.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/FSATd_to_FSATdc.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SeparationLogic/SL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LNat.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SetConstraints/Util/Facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/measure_ind.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/PCPb_to_HaltL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/notations.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Numbers.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/ZF_model.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/tactics.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA3_to_MMA2_HALTING.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/ars/normalisation.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Reductions/SysF_TYP_to_SysF_TC.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Enumerators/SBTM_HALT_enum.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_HALTING_to_MM2_HALTING.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/SBTM_to_MMA2_HALTING.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CaseNat.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_one_rel.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/FRACTRAN_to_MMA2.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/list_focus.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Reductions/iBPCP_MM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Reductions/MM_EILL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_list.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/Fin.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/Reductions/CFPI_to_CFI.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/Mirror.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/PCPb_to_MM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/minZF_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SeparationLogic/MSL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_to_MMA_HALTING.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_logic.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/MuRec_computable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/FOL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/recomp.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/RA_UNIV_HALT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/HaltMuRec_to_HaltL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareTacticsView.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Vec/vec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_utils.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/normalisation.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/TM/TapeFuns.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/beta.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_logic.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/ars/confluence.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Util/Krivine_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/FSAT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosPointers.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/VectorPrelim.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/SMNdl_UB_to_CSSM_UB.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/PCTM_HALT_to_BSM_HALTING.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/discrete.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/unification/higher_order_unification.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/BasicFinTypes.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/H10.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Tarski.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/FullTarski.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareCombinators.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/concon/conservativity_consequences.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/MuRec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/schellinx.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_UMORTAL_dec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/SBTM_HALT_to_PCTM_HALT.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Enumerators/HaltL_enum.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/FinTypeLookup.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sign1_Sig.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Util/Subterm.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Util/Diophantine.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_tac.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA2_to_MMA2_zero.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/terms_extension.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/CSSM_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/FOLFS.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/Multi.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM2.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/Undecidability.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/binZF.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Reductions/EILL_ILL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Prelim/StringBase.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Reductions/wCBNclosed_to_wCBN.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/Util/Subst.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/third_order/simplified.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/Compare.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Reductions/EILL_CLL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN_dec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/Reductions/PCP_to_CFPI.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_enum.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SetConstraints/Reductions/H10UC_SAT_to_FMsetC_SAT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/axioms.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL_full_fragment.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Kripke.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Reductions/ILL_CLL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/InformativeReducibilityFacts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Util/term_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/wf_chains.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_rem_props.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/unification/unification.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM_dec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/Code.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/iipc2_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig1.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/KOSBTM/KOSBTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/WriteString.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_elem.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/ComputableTactics.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/PA.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MPM2_HALT_dec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/finite.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_REV_dec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/calculus.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Util/Facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Basic/Basic.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_ZFD.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig0.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Lifting/Lifting.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/TM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Util/h10c_utils.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/mixedTactics.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/Combinators.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/L_enum.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/NatSub.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/SBTM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fol_ops.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/HeapInterpreter/JumpTargetTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/ArithLibs/lagrange.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Extract.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/GenericNary.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/Util/PA2_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CaseList.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/AbstractMachines/FlatPro/UnfoldClos.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM2_dec.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_in.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/BPCP_SigBPCP.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCP_to_PCPb.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_string.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Syntax_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/WriteValue.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/unscoped.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/HeapInterpreter/UnfoldClos.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/H10UC_SAT_to_H10UPC_SAT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/NatTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/bsm_mma.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/binFOL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/binomial.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/SysF.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPb_iff_BPCP.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/VectorForall.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosIncrementTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/sig_bin.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/KOSBTM/HaltKOSBTM_to_HaltKOSBTMu.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/SemiDecidabilityFacts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/std.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/PCP.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Reductions/PCPb_to_FOLFS.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/SBTM_enum.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPb_iff_dPCPb.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/Facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/bool_list.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Util/L_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/step.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/LClos.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_no_syms.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/DecidabilityFacts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/EqDec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_upto.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_no_self.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_Sig_fin.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Lrewrite.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Util/PCP_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/reductions.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/concon/constants.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareTactics.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Base.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Enumerators/SBTM_HALT_enum.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/encoding.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/MoveToSymbol.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/TMTac.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Util/Enumerable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/focus.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SeparationLogic/Reductions/FSATdc_to_MSLSAT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/CompoundFinTypes.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Prelim.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/membership.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/Compiler.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/EILL.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/Compiler_spec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/IMSELL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/ndMM2.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/sums.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/typing.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/Util/Tarski.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_nat.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/Facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_utils.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CaseCom.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN/mm_fractran.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/poly_type_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_enum.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Lifting/LiftTapes.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/ars/list_reduction.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/discernable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_eqb.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_sem_eq.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig2_Sign.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/enumerable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/KOSBTM/KOSBTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/Util/PA2_categoricity.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/H10C.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/ill_cll.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig1_1.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sign_Sig.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/ZF_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/PA2.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/L.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/compiler_correction.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/NaryApp.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/AbstractMachines/FlatPro/LM_heap_correct.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_rem_syms.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CounterMachines/Reductions/MM2_HALTING_to_CM1_HALT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Size.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/FullDeduction.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosAddTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/FullFOL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HilbertCalculi/Reductions/MPCPb_to_HSC_PRV.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/ndMM2.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/reln_hfs.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/hfs.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/Enumerable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/LClos_Eval.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/recalg.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosShiftTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/HaltTM_1_to_SBTM_HALT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN/fractran_utils.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/L_to_mTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/MPCP_to_MPCPb.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/php.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Dec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/PCP.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Krivine.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/CLL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/MuRec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/SemiU.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/concon/conservativity.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CasePair.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/countability.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_ZFeq.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/wCBN.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMenv/mme_utils.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Prelim/MoreList.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/ILL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/TM/TMEncoding.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/embed_nat.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/ArithLibs/luca.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/schellinx.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_bounded.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/ill_cll_restr.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CaseSum.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/interval.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Prelim/ARS.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Syntax.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Reductions/LU2SemiU_to_SysF_TYP.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/SMN.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/MoreEnumerabilityFacts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/BasicDefinitions.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Reductions/Diophantine_to_MuRec_computable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Acceptability.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_single.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/SR.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/If.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/evaluator.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/CFG.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/FinNotation.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/motivation.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_fold.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/H10C_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/eill_mm.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/sorting.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Lbeta_nonrefl.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/minFOL_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Reductions/FRACTRAN_computable_to_Diophantine.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/TRAKHTENBROT_to_FSAT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/StateWhile.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareLogic.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB/SMX.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CodeTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/H10Z.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/SSM.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/ComputableDemo.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Reductions/MM_FRACTRAN.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/List/Cons_constant.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/enumerable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Eval.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/red_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HilbertCalculi/HSC.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/EncodeBinNumbers.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/prime.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareTactics.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPb_iff_iPCPb.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Por.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_dec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Reductions/HaltLclosed_to_wCBNclosed.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/deterministic_simulation.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/Transcode/BoollistEnc.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/fractran_mma.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HilbertCalculi/Util/HSCFacts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Reductions/ndMM2_IMSELL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/utils.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_discernable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosCompareTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/HeapInterpreter/LookupTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/third_order/encoding.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/PCSnf.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_godel_beta.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/List/App.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/Transcode/Boollist_to_Enc.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PolynomialConstraints/LPolyNC.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/RU2SemiU_to_SemiU.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/third_order/pcp.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_definable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_congruence.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/SysF.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Basic/Duo.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/ill.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareStdLib.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/FullSyntax.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/decidable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Lbeta.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Tactics/Tactics.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_dio_poly.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/SequentialComposition.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/H10C.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_univ.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_univ_andrej.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/SBTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/eill.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/minimizer.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/typing_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/CSSM_UB_to_SSemiU.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/confluence.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_extra.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/SMN.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SeparationLogic/SL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Reflection.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/ill_cll_restr.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/lists/misc.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_mm.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/MoreReducibilityFacts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Vec/pos.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/SemiU.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Util/prime_seq.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_noeq.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/wf_incl.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_pctm.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LOptions.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/ChangeAlphabet.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_terms.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/reduction.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CounterMachines/CM1.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Decidability.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/ResourceMeasures.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SetConstraints/FMsetC.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/CFP.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FOL_intu.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/prim_min.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_cipher.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_defs.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/Vectors.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_sat_dec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/wf_finite.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/EqBool.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosHelperMachines.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/HeapInterpreter/M_LHeapInterpreter.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Reductions/EILL_ILL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LSum.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/FullDeduction_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/SSM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LProd.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Deciders/Halt_REV_FRACTRAN_dec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosMultTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/EncBoolsTM_boolList.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/DoubleNegation.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/CopySymbols.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/SSTS.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/Syntax.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/dowek/encoding.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/third_order/huet.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/List/Nth.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/sn_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/Compiler_nat_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/rel_iter.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_MM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/unification/nth_order_unification.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/lists/advanced.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM/tiles_solvable.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CompareValue.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/While.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Util/wCBN_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Numbers.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HilbertCalculi/Reductions/MPCPb_to_HSC_AX.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_utils_bsm.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/KrivineMclosed_HALT_to_HaltUTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sign_Sig2.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Reductions/wCBNclosed_to_KrivineMclosed_HALT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Reductions/SysF_TYP_to_SysF_TC.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/EILL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/unification/enumerability.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB/SMX.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/lists/basics.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_expo.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/PrettyBounds/MaxList.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_ca.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_k_mma_2_compiler.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LFinType.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/Compiler_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/seteq.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/multiplication.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/terms.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_minZFeq.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Prelim/LoopSum.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Encoding.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/AbstractMachines/FlatPro/UnfoldClos.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/red_dec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/concon/conservativity_constants.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig2_SigSSn1.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/List/Length.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMenv/env.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/iPCPb_to_BSM_HALTING.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM_2_HALTING_dec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/ComputableTime.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/imsell.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Util/List_facts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SetConstraints/Util/Facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SeparationLogic/MSL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/PCTM/pctm_sbtm.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/MuRec/MuRec_extract.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/FullTarski.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/Reductions/PCP_to_CFPP.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CaseFin.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FOL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/DPRM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/Switch.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/Reductions/CFPP_to_CFP.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/Reductions/H10p_to_SOL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/Shift.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_quotient.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/List/Rev.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_comp_strong.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/order.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_rem_cst.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/ndMM2/ndmm2_utils.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/SBTM_HALT_to_SR.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CaseBool.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/ListEnumerabilityFacts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/deterministic_simulation.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/binFOL_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/ArithLibs/matrix.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA2_to_ndMM2_ACCEPT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_rt_closure.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/unification/systemunification.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_comp.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA2_to_MM2.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/VectorDupfree.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/ars/normalisation.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Computability.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Aczel.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Util/FRACTRAN_sss.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/ClosedLAdmissible.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Retracts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/diophantine_equations.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/ListAutomation.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/TM/TMinL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/NTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/BSM_computable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/Alphabets.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Seval.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_base.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/equivalence.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/pure_term_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Prelim/MoreBase.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/Combinators.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Aczel_TD.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/concon/enumerability.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/FA_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/MMA_HALTING_n_to_HaltTM_n.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Util/H10UPC_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/Transcode/Enc_to_Boollist.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/SBTM_HALT_to_HaltBSM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/SMN_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_recomp.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Aczel_CE.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MM2_to_ndMM2_ACCEPT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/HaltTM_1_to_PCPb.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosDefinitions.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/term_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Util/FRACTRAN_computable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/list_bool.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/semantics.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Synthetic.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareMult.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/LoopSum.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/quotient.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/crt.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_defs.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MM2_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/concon/constants_consequences.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_uniform.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/FRACTRAN_DIO.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/PCTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/Util/Facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/ReducibilityFacts.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Proc.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/DepPairs.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/H10_to_L.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/MPCP_to_PCP.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Inhabited.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/retracts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/Nat_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_sig.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMenv/mme_defs.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/EnumerabilityFacts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10p_to_FA.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/wCBN.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Reductions/H10_to_H10p.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/power_decomp.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/godel_coding.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/embed_nat.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/Definitions.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/SOL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Lsimpl.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_sat.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/gfp.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/Lists.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FOL_class.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/SR.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/Prelim.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/FinTypesDef.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/ars/basic.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Lifting/LiftAlphabet.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/FRACTRAN_to_H10C_SAT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Lproc.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_simul.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig0.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/H10p.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Computable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/compiler.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/TM_computable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPX_iff_dPCP.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/syntax.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/TMTac.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/InformativeReducibilityFacts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/FullTarski_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_defs.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/subcode.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/List/Concat_Repeat.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/misc.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Lbeta.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/unscoped.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MM_to_MMA2.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/Definitions.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/CFG.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma3_mma2_compiler.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_nat.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/ZF_model.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_decidable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/SBTM_HALT_to_HaltTM_1.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/PCPb_to_HaltL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/ReducibilityFacts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/Infinite.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/bpcp.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_binary.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/AbstractMachines/FlatPro/LM_heap_def.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/KOSBTM/HaltTM_1_to_HaltKOSBTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Enumerators/term_enum.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/UpToC.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/H10_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Fractran/fractran_dio.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Krivine.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_one_rel.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MM_sss.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/acc_irr.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/BSM_sss.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_REV_dec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PolynomialConstraints/LPolyNC.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Lists/BaseLists.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Single/EncodeTapes.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_bij.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_rem_constants.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LNat.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Decoding.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/red_enum.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MM_computable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CounterMachines/Util/CM1_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM2.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/GenericNary.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/L.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/Models_Equivalent.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Matija/expo_diophantine.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/red_utils.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Util/Definitions.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/AbstractMachines/FlatPro/Programs.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/TM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_choice.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/binZF_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/dowek/reduction.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Kripke.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/UnboundIteration.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LBool.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/prelim.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CaseNat.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/Eval.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/UpToCNary.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/bounded_quantification.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Basic/Mono.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/FinTypes.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sign1_Sig.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/H10Z_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/iipc2_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/minimizer.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Reductions/H10_to_MUREC_HALTING.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Deduction.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_rem_props.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/HaltTM_1_to_MM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HilbertCalculi/HSC.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/WriteString.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/recursor.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/decidable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/SBTM_HALT_to_TSR.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Syntax.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Compound/Multi.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CounterMachines/CM1.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/PrettyBounds/SizeBounds.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Util/Krivine_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB/SMX_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/Tarski.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/ars/confluence.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Ackermann.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/SR_to_PCSnf.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_simul.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig1.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/measure_ind.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LVector.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/minZF_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/VectorFin.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/SR_to_MPCP.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/ars/list_reduction.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_UMORTAL_dec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/IMSELL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/step.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Util/term_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/FullTarski.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/CFP.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/bsm_mma.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/ars/evaluator.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PolynomialConstraints/Reductions/FMsetC_SAT_to_LPolyNC_SAT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_pcp.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/focus.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MM2_HALTING_to_MM2_ZERO_HALTING.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/TM_to_L.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_string.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/acc_irr.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/EqDecDef.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosIncrementTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/SBTM_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/normalisation.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/wf_chains.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/Mirror.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_enum.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/Reductions/PCP_to_CFPI.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_no_syms.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/SMNdl_UB_to_CSSM_UB.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Util/Facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/Relations.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_noeq.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/H10SQC_SAT_to_H10UC_SAT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/HaltTM_1_chain_SemiU.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_in.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/PCTM/pctm_defs.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/ILL_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/GenEncode.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/InformativeDefinitions.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/PCSnf.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_tac.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sign_Sig.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_enum.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/wf_incl.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/MuRec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA3_to_MMA2_HALTING.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/recomp.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/FSAT_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Autosubst/unscoped.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/SSTS.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Partial.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_basics.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/PosPointers.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/beta.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/ZF.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/ComputableDemo.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_sem_eq.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/PCP_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/Util/axioms.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Enumerators/HaltL_enum.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/minZF.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig2_Sign.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Fixpoints.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/AbstractMachines/LargestVar.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/RU2SemiU_to_LU2SemiU.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/EqDec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/list_focus.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Ll/ill_cll.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/ndMM2.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_upto.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/discernable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/FSAT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Util/Subterm.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/TRAKHTENBROT_to_FSAT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/Undecidability.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LTerm.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/TM/TMinL/TMinL_extract.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CaseCom.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/BasicFinTypes.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fol_ops.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Dec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/TM/TapeFuns.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/Fin.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/notations.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/AbstractMachines/FlatPro/ProgramsDef.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Basic/Null.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/List_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareLegacy.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/H10.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/focus.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/minFOL_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Util/PCP_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCP_to_PCPb.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/binomial.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SetConstraints/FMsetC.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_expo.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/FOL_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Tactics/AutoIndTac.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/SSemiU_to_RU2SemiU.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/InformativeDefinitions.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Util/h10c_utils.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/DecidabilityFacts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_to_MMA_HALTING.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Equality.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/typing.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/unification/higher_order_unification.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/H10C_SAT_to_H10SQC_SAT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/PA.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/TM/TMEncoding.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Reductions/MM_EILL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/BinNumbers/EncodeBinNumbers.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_eqb.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/WriteValue.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/FinTypeLookup.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/ZF_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/FinNotation.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/axioms.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/KOSBTM/HaltKOSBTM_to_HaltKOSBTMu.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/MuRec_computable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Lsimpl.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Tactics/Tactics.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/H10Z.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/unscoped.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/CompoundFinTypes.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/notations.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Reductions/Diophantine_to_MuRec_computable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/mTM_to_TM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/RU2SemiU_to_SemiU.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/FRACTRAN_to_MMA2.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/FinTypesDef.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/NatSub.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM/tiles_solvable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_discrete.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/third_order/simplified.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/reductions.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/H10UC_SAT_to_H10UPC_SAT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Eval.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/deterministic_simulation.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LOptions.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/PCP.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Lbeta_nonrefl.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/ReducibilityFacts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_cipher.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/interval.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Subst.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/LClos_Eval.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Acceptability.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/Facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/L_computable_to_TM_computable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/red_utils.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/Lproc.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Enumerators/SBTM_HALT_enum.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/LComp_to_TMComp.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/NaryApp.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/SemiU_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_godel_beta.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/SysF.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_sig.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/countability.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/wf_finite.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/If.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/BasicDefinitions.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/H10C.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMenv/env.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/DiophantineConstraints/H10C_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/utils.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/H10p.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Reductions/H10C_SAT_to_RA_UNIV_HALT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LSum.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/Reductions/CFPI_to_CFI.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/ListAutomation.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/EILL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Prelim/MoreList.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Por.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/ArithPrelim.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/Facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_dec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/SemiU.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LProd.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/FOL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Reductions/MM_FRACTRAN.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/confluence.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/PCTM_HALT_to_BSM_HALTING.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Reductions/EILL_CLL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/FOLFS.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HilbertCalculi/Util/HSCFacts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Size.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/MoreEnumerabilityFacts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/VectorForall.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/prim_min.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/binZF.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Dio/dio_rt_closure.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/PA2.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/lists/misc.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/fo_sat.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM2_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/List/Cons_constant.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CaseFin.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/FRACTRAN_DIO.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/ProgrammingTools.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/iPCPb_to_BSM_HALTING.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/HaltL_to_HaltLclosed.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/VectorDupfree.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Inhabited.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/PCPb_to_MM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Tactics/Tactics.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM2_dec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Util/Enumerable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Computability.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/FSATd_to_FSATdc.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/SysF_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/H10_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/PCTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Util/List_facts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/ILL_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/MuRec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/HaltTM_1_chain_SemiU.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Reductions/FRACTRAN_computable_to_Diophantine.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/EqDecDef.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Decidability.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/MuRec/MuRec_extract.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_fold.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Util/pure_term_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MM_to_MMA2.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/MPCP_to_MPCPb.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareStdLib.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Reductions/SysF_TYP_to_SysF_TC.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/ProgrammingTools.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FOL_intu.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Util/Diophantine.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/KrivineMclosed_HALT_to_HaltUTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MUREC_MM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/evaluator.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/Reductions/PCP_to_CFPP.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LFinType.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/IMSELL_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPb_iff_iPCPb.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/HaltL_to_HaltTM_5.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Reductions/HaltTM_1_to_SysF_TYP.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Basic/Duo.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/Transcode/BoollistEnc.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/CaseBool.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/MoreReducibilityFacts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/Undecidability.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/EqBool.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Prelim/StringBase.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/ndMM2/ndmm2_utils.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Reductions/wCBNclosed_to_KrivineMclosed_HALT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/VectorPrelim.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/third_order/pcp.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/HaltTM_1_to_PCPb.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LBool.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/wCBN_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/Definitions.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/LinDecode/LTD_def.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Encoding.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Reductions/HaltTM_1_to_SysF_INH.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/SBTM_HALT_to_PCTM_HALT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Util/wCBN_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/Alphabets.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Reductions/H10C_SAT_to_RA_UNIV_HALT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Util/FRACTRAN_sss.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/PA_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/FullDeduction.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Reductions/ILL_CLL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/FullTarski.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Prelim/MoreBase.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/Compiler_spec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Reductions/wCBNclosed_to_wCBN.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Reductions/MM_computable_to_FRACTRAN_computable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareTacticsView.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CounterMachines/Reductions/HaltTM_1_to_CM1_HALT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/Lists.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/SBTM_to_MMA2_HALTING.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Reductions/iBPCP_MM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/SMN.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/red_enum.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HilbertCalculi/HSC.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/SSM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TRAKHTENBROT/Sig_discrete.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/SBTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Reductions/HaltTM_1_to_FRACTRAN_HALTING.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/SBTM_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Combinators/SequentialComposition.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Reductions/H10_to_H10p.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/BSM_computable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_string.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_enc.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Proc.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_HALTING_to_MM2_HALTING.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/FRACTRAN_to_MMA2.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/MuRec_computable_to_L_computable.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PolynomialConstraints/LPolyNC.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/HaltTM_1_to_SemiU.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/Enumerable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/concon/constants_consequences.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/FOL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_MM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/KOSBTM/KOSBTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA2_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HilbertCalculi/HSC_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SetConstraints/FMsetC.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/UTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Numbers.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_extra.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/list_focus.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/SemiDecidabilityFacts.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/concon/conservativity_consequences.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Krivine_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SetConstraints/Util/Facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/SemiU_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma3_mma2_compiler.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/TM/TMinL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Util/FRACTRAN_computable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/TM_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/ars/normalisation.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/TM_computable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/tactics.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/recursor.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/PA2_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPb_iff_BPCP.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/acc_irr.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA2_to_MMA2_zero.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Prelim/LoopSum.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_simul.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/wCBN.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Reductions/H10_to_MUREC_HALTING.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/SR_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/PCP_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/L_to_mTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/LoopSum.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SeparationLogic/SL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Partial.vo../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM2_dec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/tactics.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPb_iff_dPCPb.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/motivation.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/RA_UNIV_HALT.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/retracts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareTacticsView.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Reductions/EILL_ILL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPX_iff_dPCP.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Krivine.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/Fin.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/FSAT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/binZF_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/HaltTM_1_to_CSSM_UB.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CounterMachines/CM1.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/CFG_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/CFG.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/L.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/RA_UNIV_HALT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/FOL_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/Util/Facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB/SMX.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/SOL_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Reductions/MM_EILL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/beta.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/HaltTM_1_to_MM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SeparationLogic/MSL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MUREC_MM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/CFP_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/VectorFin.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/misc.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/HaltTM_1_to_PCP.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/Models_Equivalent.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SeparationLogic/Reductions/MSLSAT_to_SLSAT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM2_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/H10.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/HaltTM_1_to_iPCPb.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/InformativeReducibilityFacts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/second_order/diophantine_equations.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/Nat_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/IMSELL_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Ackermann.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/embed_nat.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/DepPairs.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/SSTS.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/SR.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/SysF_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Reductions/iBPCP_MM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/LinDecode/LTDlist.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Enumerators/term_enum.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/PCPb_to_MM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/ndMM2/ndmm2_utils.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA3_to_MMA2_HALTING.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/SBTM_to_MMA2_HALTING.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/BasicFinTypes.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HilbertCalculi/HSC_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/CLL_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Tactics/AutoIndTac.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LTerm.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/FinTypesDef.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/PCTM_HALT_to_BSM_HALTING.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PolynomialConstraints/LPolyNC_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_to_MMA_HALTING.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Equality.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/FSAT_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/TM_to_L.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA2_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/RA_UNIV_HALT_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/CLL_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/HaltTM_1_to_SR.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SetConstraints/FMsetC_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Reductions/HaltTM_1_to_SysF_TC.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MM_computable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/ndMM2_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/wCBN_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/binFOL_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/SSTS_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/UTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_nat.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CounterMachines/CM1_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/CFP.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/SBTM_HALT_to_PCTM_HALT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA2_to_MMA2_zero.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/H10p.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/L_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Enumerators/HaltL_enum.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/SSM_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Reductions/HaltTM_1_to_SysF_TYP.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/UTM_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/AbstractMachines/LargestVar.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/PCSnf_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/sig_bin.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Reductions/EILL_CLL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Basic/Null.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/SMN_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM/tiles_solvable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Krivine_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/ndMM2_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Reductions/HaltTM_1_to_SysF_INH.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SeparationLogic/SL_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/MuRec_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Fixpoints.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Reductions/FSATd_to_FSATdc.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/RU2SemiU_to_SemiU.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/PCSnf.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SeparationLogic/MSL_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/ILL/Reductions/ILL_CLL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/LambdaCalculus/Reductions/wCBNclosed_to_wCBN.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/H10p_undec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/HaltTM_1_to_SemiU.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/BSM_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/axioms.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM_dec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/std.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CounterMachines/Reductions/HaltTM_1_to_CM1_HALT.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Util/Subterm.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/Reductions/HaltTM_1_to_FRACTRAN_HALTING.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/mixedTactics.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/MuRec_computable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN_dec.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/SBTM_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOLP/FOLFS.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/Hoare.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CounterMachines/CM1_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN_dec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/LinDecode/LTDbool.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/LinDecode/LTDnat.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_HALTING_to_MM2_HALTING.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/HaltL_to_HaltTM_5.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/PA_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/ArithPrelim.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SetConstraints/FMsetC_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PolynomialConstraints/LPolyNC_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/L/CompilerBoolFuns/LComp_to_TMComp.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Reductions/L_computable_to_TM_computable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/Reductions/CFPI_to_CFI.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/TM_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/ListTM.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/SMN_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/HaltTM_1_to_CSSM_UB.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/finite.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/SSM_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/EqDecDef.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/SBTM_enum.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/SR_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/calculus.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/HaltL_to_HaltLclosed.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/CFG_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Prelim/StringBase.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/CFG/CFP_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/binFOL.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/AbstractMachines/FlatPro/ProgramsDef.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Reductions/MuRec_computable_to_L_computable.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/HaltTM_1_to_PCP.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SystemF/Reductions/HaltTM_1_to_SysF_TC.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/HaltTM_1_to_iPCPb.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/L_enum.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StackMachines/Util/Facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Util/VectorPrelim.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/PrettyBounds/SizeBounds.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/PA2_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/LTactics.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MinskyMachines/MM_dec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/Util/RA_UNIV_HALT_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/axioms.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPb_iff_BPCP.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_enc.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/InformativeDefinitions.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/finite.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/HoareLegacy.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/binFOL.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Prelim.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Functions/Subst.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LUnit.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SOL/SOL_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Prelim.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/L_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/HaltTM_1_to_SR.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/concon/conservativity_consequences.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/Util/List_facts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/mixedTactics.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/LinDecode/LTDlist.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/Util/Diophantine.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/SSTS_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/LinDecode/LTD_def.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/StringRewriting/PCSnf_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Synthetic/SemiDecidabilityFacts.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Hoare/Hoare.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/LinDecode/LTDnat.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/H10/H10p_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/MuRec/MuRec_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/UTM_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Complexity/LinDecode/LTDbool.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPb_iff_dPCPb.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/std/std.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/unification/unification.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Datatypes/LUnit.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SeparationLogic/MSL_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Base.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Tactics/LTactics.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/SBTM_enum.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Code/ListTM.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/SeparationLogic/SL_undec.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/FOL/Util/sig_bin.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/L_enum.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Base.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/calculus/calculus.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Basic/Basic.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Lifting/Lifting.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Tactics/AutoIndTac.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/HOU/unification/unification.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/L/Computability/Partial.glob../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Lifting/Lifting.v../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Undecidability/TM/Basic/Basic.vopam remove -y coq-library-undecidability.1.0.1+8.16