# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-domains base
base-nnp base Naked pointers prohibited in the OCaml heap
base-threads base
base-unix base
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq 8.17.0 The Coq Proof Assistant
coq-core 8.17.0 The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib 8.17.0 The Coq Proof Assistant -- Standard Library
coqide-server 8.17.0 The Coq Proof Assistant, XML protocol server
dune 3.13.0 Fast, portable, and opinionated build system
ocaml 5.0.0 The OCaml compiler (virtual package)
ocaml-base-compiler 5.0.0 Official release 5.0.0
ocaml-config 3 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.6 A library manager for OCaml
zarith 1.13 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.17.0"}
"ocaml"
"coq-metacoq-template" {>= "1.2+8.17"}
]
synopsis: "A Coq Library of Undecidability Proofs"
url {
src: "https://github.com/uds-psl/coq-library-undecidability/archive/refs/tags/v1.1+8.17.tar.gz"
checksum: "sha256=7a17e6a5e9c016f660b7074b42524aaa9656288bea3c1a3b7e7af303d4375472"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-library-undecidability.1.1+8.17 coq.8.17.0Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; timeout 4h opam install -y --deps-only coq-library-undecidability.1.1+8.17 coq.8.17.0opam list; echo; timeout 4h opam install -y -v coq-library-undecidability.1.1+8.17 coq.8.17.0Total: 106 M
../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB/CM1_to_SMX.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_minZF.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_rem_cst.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Matija/cipher.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_binZF.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB/CM1_to_SMX.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Single/StepTM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_minZF.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/PCPb_to_HaltL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FSAT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_elem.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/TM_computable_to_BSM_computable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/BPCP_SigBPCP.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/L_computable_to_MMA_computable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/MM2_ZERO_HALTING_to_SSTS01.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/Arbitrary_to_Binary.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/L_computable_to_MMA_computable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_utils.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_basics.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/pure_typable_prenex.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Reductions/H10C_SAT_to_SysF_INH.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_no_self.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_utils.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/TM_computable_to_BSM_computable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_utils.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Deduction/FullNDFacts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_mm_env.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/MuRec/MuRec_extract.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/MM2_ZERO_HALTING_to_SSTS01.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_utils.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Single/StepTM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_univ_andrej.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_utils.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Matija/alpha.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Matija/cipher.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FSAT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_eqb.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/KOSBTM/HaltKOSBTM_to_HaltBSM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_REV_HALT_dec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/HaltMuRec_to_HaltL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_binZF.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_UBOUNDED_dec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_pcp.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/gcd.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FSAT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL_constructions.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/SMN_transform.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Autosubst/syntax.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/H10_to_L.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/bool_nat.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/Util/PA2_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Reductions/H10C_SAT_to_SysF_INH.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/firstorder.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/ZF_conservativity.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_computable_to_MM_computable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Reflection.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/KOSBTM/HaltKOSBTM_to_HaltBSM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/bool_nat.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_computable_to_MM_computable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_mm_env.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FSTD.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/KrivineMclosed_HALT_to_MMA_HALTING.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Matija/alpha.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Compound/MoveToSymbol.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_ca.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/KrivineMclosed_HALT_to_HaltUTM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_HFD.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SetConstraints/Reductions/H10UC_SAT_to_FMsetC_SAT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/SMN_transform.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FSAT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_bounded.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMenv/mme_utils.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/ArithLibs/Zp.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL_constructions.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_fold.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FST.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_single.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_utils.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_ZFD.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/CSSM_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/H10Z_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/schellinx.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Deduction/FragmentNDFacts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/KrivineMclosed_HALT_to_MMA_HALTING.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_REV_HALT_dec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/pure_typing_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_ZF.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_HF.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MPM2_HALT_dec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_UBOUNDED_dec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_list.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/sss.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/ArithLibs/lagrange.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/ArithLibs/luca.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HilbertCalculi/Reductions/MPCPb_to_HSC_PRV.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_dio_poly.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL_full_fragment.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/pure_typable_prenex.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/ArithLibs/Zp.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/btree.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LNat.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/KOSBTM/HaltTM_1_to_HaltKOSBTM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/sorting.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_Sig_fin.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/ZF_conservativity.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/firstorder.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SetConstraints/Reductions/H10UC_SAT_to_FMsetC_SAT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CounterMachines/Reductions/MM2_HALTING_to_CM1_HALT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/Arbitrary_to_Binary.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/Util/Tarski.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/pure_typing_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Util/TM_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_logic.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Util/L_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Compound/Shift.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Deduction/FullNDFacts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA_computable_to_MMA_mon_computable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SeparationLogic/Reductions/FSATdc_to_MSLSAT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/reln_hfs.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/btree.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/terms_extension.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/Util/Syntax.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/HaltTM_1_to_SBTM_HALT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/gcd.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Vec/vec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_HFD.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL_friedman.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/AbstractMachines/wCBV.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/TM/TapeFuns.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/MMA_mon_computable_to_TM_computable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Synthetic.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FSTD.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/FiniteTarski/DoubleNegation.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/TM/TMEncoding.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_ZFD.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_nat.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Extract.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN/mm_fractran.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_utils.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/CSSM_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MMA_pairing.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/sss.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_logic.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_cipher.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_list.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/eill_mm.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Vec/vec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_univ.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Util/PCP_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/Util/PA2_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MPM2_HALT_dec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/discrete.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/SBTM_HALT_to_HaltBSM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/HaltTM_1_to_SBTM_HALT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/encoding.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/ArithLibs/lagrange.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/multiplication.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/prime.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MMA_pairing.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Deduction/FragmentNDFacts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_binary.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/dowek/encoding.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM_2_HALTING_dec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA_computable_to_MMA_mon_computable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_congruence.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_utils.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CounterMachines/Reductions/MM2_HALTING_to_CM1_HALT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_discernable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/third_order/encoding.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/reduction.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_rem_syms.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL_full_fragment.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Autosubst/syntax.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/ZF_model.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/SBTM_HALT_to_HaltBSM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/poly_type_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/Bounded.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig2_SigSSn1.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_ZFeq.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/sums.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/binZF_to_binFST.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Util/ClosedLAdmissible.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/SBTM_HALT_to_SR.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LTerm.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_ZF.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Deciders/Halt_REV_FRACTRAN_dec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FST.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_logic.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Matija/expo_diophantine.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/fractran_mma.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/Eval.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HilbertCalculi/Reductions/MPCPb_to_HSC_PRV.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/terms_extension.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/concon/constants.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/sums.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/recalg.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/recomp.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/BPCP_SigBPCP.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/membership.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/MMA_mon_computable_to_TM_computable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/ArithLibs/luca.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Util/TM_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/CSSM_UB_to_SSemiU.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_HF.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA2_to_ndMM2_ACCEPT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/third_order/huet.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_nat.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_mm.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/fractran_mma.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/HaltMuRec_to_HaltL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/discrete.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/concon/constants.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/step.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/Encoding.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_expo.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SeparationLogic/Reductions/FSATdc_to_MSLSAT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/power_decomp.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_utils_bsm.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/SBTM_HALT_to_HaltTM_1.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/encoding.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LVector.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_REV_dec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Util/H10UPC_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/HF_model.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/DiscreteEnumerable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LOptions.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/CSSM_UB_to_SSemiU.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/SMN_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/membership.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_Sig_fin.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/concon/conservativity.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/php.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Reductions/HaltLclosed_to_wCBNclosed.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/Util/PA2_categoricity.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_logic.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MM2_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig1_1.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Tarski/FragmentFacts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/StateWhile.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_no_self.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN/fractran_utils.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/bool_list.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HilbertCalculi/Reductions/MPCPb_to_HSC_AX.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/compiler_correction.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/AbstractMachines/wCBV.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_minZFeq.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/SBTM_HALT_to_SR.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN/mm_fractran.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/ZF_model.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/bool_list.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Reductions/LU2SemiU_to_SysF_TYP.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Util/prime_seq.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/Asimpl.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMenv/mme_utils.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/hfs.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/semantics.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/Util/Syntax.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_elem.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Single/StepTM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/rel_iter.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/TM/TMinL/TMinL_extract.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/MMA_HALTING_n_to_HaltTM_n.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_defs.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/Util/PA2_categoricity.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Compound/MoveToSymbol.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/enumerable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_ZFeq.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/Reductions/CFPP_to_CFP.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_pctm.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/MPCP_to_PCP.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/concon/conservativity_constants.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/reduction.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/PCTM/pctm_sbtm.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_nat.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/ArithLibs/matrix.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/typing_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_extra.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/SBTM_HALT_to_TSR.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/LClos.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/poly_type_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/FinNotation.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB/CM1_to_SMX.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/concon/conservativity.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Vec/pos.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Prelim/ARS.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/order.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_enum.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_utils_bsm.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_pctm.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/sn_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/compiler_correction.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/FST_model.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LSum.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LProd.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/hfs.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_sat_dec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_defs.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/unification/systemunification.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/crt.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Reductions/LU2SemiU_to_SysF_TYP.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Util/SBTM_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Reductions/ndMM2_IMSELL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/MuRec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/unification/nth_order_unification.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10p_to_FA.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FOL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMenv/mme_defs.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/sorting.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_univ_andrej.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/Switch.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Extract.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MM2_to_ndMM2_ACCEPT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_definable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/Equality.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_recomp.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/StateWhile.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/subcode.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_rem_constants.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/Proc.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL_friedman.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_defs.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/equivalence.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MM_sss.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_discernable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/HF_model.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Computable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_single.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/recalg.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig1_1.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Utils/FriedmanTranslation.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/compiler.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/BSM_sss.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/H10SQC_SAT_to_H10UC_SAT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/Subst.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Reflection.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_k_mma_2_compiler.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/FinTypeLookup.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Lrewrite.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/ComputableTactics.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Reductions/ndMM2_IMSELL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/EnumerabilityFacts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_decidable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/Util/Tarski.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/While.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_terms.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/unification/nth_order_unification.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/list_bool.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_defs.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_base.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/lists/advanced.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Kripke/FragmentSoundness.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_rem_syms.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/decidable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/While.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_comp_strong.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Por.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/Reductions/PCP_to_CFPI.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FOL_class.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/red_chain_undec_full.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_univ.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Tarski/FullFacts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/DPRM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Util/L_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/multiplication.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CounterMachines/Util/CM1_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_quotient.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/enumerable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Reductions/HaltLclosed_to_wCBNclosed.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/syntax.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/ZF_to_FST.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Rice.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_in.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Kripke/FragmentCore.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM_2_HALTING_dec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_congruence.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sign1_Sig.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/godel_coding.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/quotient.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_one_rel.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Acceptability.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/third_order/encoding.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FSAT_direct_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Util/PCP_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/GenEncode.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/ill.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/enumerable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/seteq.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_minZFeq.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/dowek/encoding.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/PCTM/pctm_sbtm.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/eill_mm.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Util/Facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LBool.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sign_Sig2.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FOL_class.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA2_to_MM2.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/ZF_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/reln_hfs.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_enc.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/FRACTRAN_to_H10C_SAT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/php.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/SR_to_MPCP.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Deciders/Halt_REV_FRACTRAN_dec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Single/EncodeTapes.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HilbertCalculi/Reductions/MPCPb_to_HSC_AX.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/Ackermann.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Autosubst/syntax.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/terms.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/term_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Util/TM_computable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_comp_strong.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/SMNdl_UB_to_CSSM_UB.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/imsell.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/typing_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/CLL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_dio_poly.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Tarski/FragmentFacts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/prelim.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/Reductions/H10p_to_SOL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_definable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_bounded.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Lbeta.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_uniform.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_comp.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/sn_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/SyntacticOps.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Matija/cipher.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/Models_Equivalent.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/TRAKHTENBROT_to_FSAT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/eill.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_defs.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Seval.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/third_order/simplified.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Util/prime_seq.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/third_order/huet.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10p_to_FA.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/minZF_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/SSemiU_to_RU2SemiU.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/ars/list_reduction.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/lists/basics.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_comp.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/ArithLibs/matrix.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/Core.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/gfp.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FOL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/Reductions/CFPP_to_CFP.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN/fractran_utils.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Utils/FriedmanTranslationFragment.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/eill.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMenv/mme_defs.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Compound/Shift.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Decidability.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/crt.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/EqDec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/FST_model.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_UMORTAL_dec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Util/H10UPC_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB/SMX_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/CLL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/terms.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/dowek/reduction.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/EnumerabilityFacts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Util/NaryApp.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_bij.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/Asimpl.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/EqBool.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/rel_iter.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Scott.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Tarski/FullSoundness.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/decidable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Reductions/FRACTRAN_computable_to_Diophantine.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/Infinite.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/prime.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/ListEnumerabilityFacts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/ILL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/TM/TMinL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/Subst.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig2_SigSSn1.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Util/Prelim.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/seteq.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/SMN_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Lsimpl.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MM2_HALTING_to_MM2_ZERO_HALTING.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FST_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_ca.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/unification/systemunification.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_no_syms.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_utils.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FSAT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PolynomialConstraints/Reductions/FMsetC_SAT_to_LPolyNC_SAT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/mTM_to_TM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_k_mma_2_compiler.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Vec/pos.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/SOL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/ILL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig0.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/L_computable_to_MMA_computable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/Bounded.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_rem_props.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_terms.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/typing.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_upto.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/BSM_computable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/List_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/ill_cll_restr.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/normalisation.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Util/Krivine_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_sat_dec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/Util/Definitions.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/TM_to_L.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/decidable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/MPCP_to_PCP.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_defs.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig1.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/FinTypes.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sign_Sig2.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Lbeta_nonrefl.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/minFOL_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/iipc2_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/UTM_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/TM_computable_to_BSM_computable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA2_to_MM2.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Utils/FriedmanTranslation.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Fractran/fractran_dio.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/MMA_HALTING_n_to_HaltTM_n.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/Aczel_TD.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/Theories.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/red_dec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/power_decomp.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Computability.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/Reductions/H10p_to_SOL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LFinType.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/IMSELL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/Switch.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/Mirror.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_enum.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/H10SQC_SAT_to_H10UC_SAT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_mm.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Reductions/H10C_SAT_to_SysF_INH.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/DeductionFacts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/order.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/H10C_SAT_to_H10SQC_SAT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/binomial.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/DiscreteEnumerable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Util/term_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/bool_nat.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/godel_coding.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/concon/conservativity_constants.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/SysF_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/Signature.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/minZF.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Krivine_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Reductions/MM_computable_to_FRACTRAN_computable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/SR_to_PCSnf.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/H10_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_binZF.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Reductions/Diophantine_to_MuRec_computable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Lproc.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/wCBN_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/FiniteTarski/DoubleNegation.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/lists/advanced.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_minZF.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/DeductionFacts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Basic/Mono.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/binFOL_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/confluence.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/dowek/reduction.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/red_chain_undec_full.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCP_to_PCPb.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/MuRec_computable_to_L_computable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/L_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_simul.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Util/Relations.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FSAT_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LUnit.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/binZF_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/prim_min.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/subcode.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/bounded_quantification.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MM2_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/Aczel_TD.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_godel_beta.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Matija/alpha.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/PA_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/LClos.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Code/Code.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/HaltL_to_HaltTM_5.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/Nat_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/wf_chains.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/L_computable_to_TM_computable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/Aczel_CE.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/Aczel.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/Aczel.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Deduction/FullND.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_mm_env.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/binFST_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_noeq.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SeparationLogic/SL_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Fixpoints.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SeparationLogic/MSL_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sign_Sig.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Prelim/ARS.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Compound/WriteString.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/MoreEnumerabilityFacts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/ill.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Synthetic.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/unification/higher_order_unification.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/pure_typable_prenex.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/H10UC_SAT_to_H10UPC_SAT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/imsell.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/DecidabilityFacts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/term_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_base.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/H10C_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/ZF.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/HaltL_to_HaltLclosed.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/SBTM_HALT_to_HaltTM_1.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/HaltTM_1_chain_SemiU.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/iPCPb_to_BSM_HALTING.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/TarskiFacts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/SemiU_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/PA2_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/Util/Subst.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_rem_cst.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/SOL_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/MuRec_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/Aczel_CE.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/Facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Compound/TMTac.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/ars/confluence.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/RA_UNIV_HALT_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/PCTM/pctm_defs.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/If.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/ListEnumerabilityFacts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/red_dec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fol_ops.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Util/ClosedLAdmissible.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_REV_HALT_dec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FOL_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Tarski/FragmentSoundness.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HilbertCalculi/Util/HSCFacts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB/SMX_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL_constructions.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PolynomialConstraints/LPolyNC_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/ILL_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA2_to_ndMM2_ACCEPT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/lists/misc.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/H10p_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/CompoundFinTypes.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/SSM_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/minimizer.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SetConstraints/FMsetC_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/SMN_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_uniform.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/ars/evaluator.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/IMSELL_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/compiler.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/ill_cll.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/bsm_mma.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPb_iff_iPCPb.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/binZF.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/RU2SemiU_to_LU2SemiU.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/SMN_transform.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/discernable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Reductions/HaltTM_1_to_SysF_TC.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_sem_eq.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Reductions/HaltTM_1_to_SysF_TYP.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/unscoped.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/Subst.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/firstorder.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Tarski/FragmentCore.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/minZF_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/third_order/pcp.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CounterMachines/CM1_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/H10_to_L.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/ars/basic.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig2_Sign.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/Reductions/PCP_to_CFPP.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/ListAutomation.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_rt_closure.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_bij.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM2_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/MM2_ZERO_HALTING_to_SSTS01.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/SSTS_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/CLL_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/motivation.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/countability.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/H10Z.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/PCP_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/NatModel.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/quotient.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Matija/expo_diophantine.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/ndMM2_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/HaltTM_1_to_SemiU.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA2_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/BSM_sss.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CounterMachines/Util/CM1_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/mTM_to_TM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/Combinators.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MM2_to_ndMM2_ACCEPT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Reductions/HaltTM_1_to_SysF_INH.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/ArithLibs/Zp.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MM_sss.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/Lists.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/VectorFin.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Utils/FriedmanTranslationFragment.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HilbertCalculi/HSC_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/CFG_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FOL_intu.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_choice.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/MoreReducibilityFacts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Util/FRACTRAN_computable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MMA_computable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/measure_ind.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/ZF_to_HF.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/CFP_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/list_bool.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/HaltTM_1_to_CSSM_UB.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MM2_HALTING_to_MM2_ZERO_HALTING.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/Arbitrary_to_Binary.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_recomp.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma3_mma2_compiler.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_binary.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/SyntacticOps.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Kripke/FragmentCore.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Reductions/MM_FRACTRAN.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/enumerable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/RU2SemiU_to_LU2SemiU.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Util/wCBN_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/ZF.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/Util/Facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/LTactics.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/btree.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/TM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/wf_incl.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/FiniteTarski/Listability.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Deduction/FragmentND.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/FRACTRAN_DIO.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/minZF.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Tarski/FullFacts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/pure_typing_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CounterMachines/Reductions/HaltTM_1_to_CM1_HALT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/interval.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_choice.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/HaltTM_1_to_PCPb.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/SSemiU_to_RU2SemiU.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/concon/constants_consequences.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Reductions/H10_to_H10p.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/BasicDefinitions.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/FST.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_sig.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/wf_finite.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/MuRec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/SR_to_PCSnf.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Dec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Reductions/MM_computable_to_FRACTRAN_computable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Tarski/FullCore.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_computable_to_MM_computable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_simul.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_MM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Rice.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/ZF_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_sat.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/equivalence.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Reductions/wCBNclosed_to_KrivineMclosed_HALT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MM_computable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/SequentialComposition.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_decidable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/DPRM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Kripke/FragmentToTarski.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/FRACTRAN_to_H10C_SAT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/red_utils.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Reductions/HaltTM_1_to_FRACTRAN_HALTING.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/bpcp.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Reductions/H10_to_MUREC_HALTING.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_quotient.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/FA.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/pure_term_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Computable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/HaltTM_1_to_iPCPb.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/HaltTM_1_to_MM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/utils.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/SBTM_HALT_to_TSR.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/binFST.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/HaltTM_1_to_PCP.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/red_enum.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PolynomialConstraints/Reductions/FMsetC_SAT_to_LPolyNC_SAT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/sss.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/gfp.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/Reductions/CFPI_to_CFI.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Autosubst/unscoped.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MUREC_MM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_dec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_discrete.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Util/h10c_utils.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Util/FRACTRAN_sss.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Util/TM_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/FiniteTarski/Full.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/DepPairs.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Autosubst/unscoped.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/PA2.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_tac.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/syntax.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/FSATd_to_FSATdc.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_pcp.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/semantics.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/ZF.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FST.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/prelim.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/decidable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/UTM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/misc.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/Infinite.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/FiniteTarski/Fragment.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/evaluator.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/SR_to_MPCP.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/H10C_SAT_to_H10SQC_SAT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Util/SBTM_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Util/Enumerable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/diophantine_equations.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Inhabited.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/gcd.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMenv/env.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/KOSBTM/HaltKOSBTM_to_HaltBSM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FOL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/MPCP_to_MPCPb.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Enumerators/term_enum.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/Vectors.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/GenEncode.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/PCTM/pctm_defs.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/retracts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL_minimal.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_rem_constants.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/KOSBTM/HaltTM_1_to_HaltKOSBTM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MM_to_MMA2.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/recursor.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM2.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/SOL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_UBOUNDED_dec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/Enumerable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Basic/Mono.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Compound/Multi.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/bounded_quantification.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPX_iff_dPCP.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/H10Z_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Reductions/iBPCP_MM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/List_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/PCTM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/PCPb_to_MM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Reductions/H10C_SAT_to_RA_UNIV_HALT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/PA.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/KrivineMclosed_HALT_to_MMA_HALTING.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Fractran/fractran_dio.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_one_rel.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_utils.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/TM_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SeparationLogic/Reductions/MSLSAT_to_SLSAT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_simul.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/PA.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SetConstraints/Util/Facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Signatures.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/notations.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/measure_ind.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FSAT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA3_to_MMA2_HALTING.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Reductions/SysF_TYP_to_SysF_TC.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Enumerators/SBTM_HALT_enum.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/Core.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_HALTING_to_MM2_HALTING.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Lrewrite.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/FRACTRAN_to_MMA2.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/list_focus.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/lists/basics.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Util/Prelim.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/SBTM_to_MMA2_HALTING.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FSAT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Reductions/MM_EILL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Vec/vec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/PCPb_to_HaltL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/ZF_to_FST.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_list.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/tactics.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/PCSnf_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_to_MMA_HALTING.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/MMA_computable_to_TM_computable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/SR_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/MuRec_computable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/SBTM_undec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/RA_UNIV_HALT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_logic.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/recomp.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Util/Relations.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/HaltMuRec_to_HaltL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_utils.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/beta.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sign1_Sig.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Kripke/FragmentSoundness.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/normalisation.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/HaltTM_1_to_SR.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/Robinson.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_logic.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Util/Krivine_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/ars/evaluator.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/SMNdl_UB_to_CSSM_UB.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/ars/confluence.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/H10.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/discrete.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/unification/higher_order_unification.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/PCTM_HALT_to_BSM_HALTING.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/BasicFinTypes.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/TarskiFacts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/binZF_to_binFST.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/MuRec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/schellinx.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Deduction/FragmentNDFacts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/concon/conservativity_consequences.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_UMORTAL_dec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Util/Diophantine.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/SBTM_HALT_to_PCTM_HALT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA2_to_MMA2_zero.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Deduction/FragmentNDConsistency.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/terms_extension.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_tac.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM2.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Enumerators/HaltL_enum.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Reductions/EILL_ILL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/CSSM_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/Undecidability.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_rem_props.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/Util/Syntax.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/Mirror.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/FinTypes.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Reductions/EILL_CLL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN_dec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Deduction/FullNDFacts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/Util/Subst.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Reductions/wCBNclosed_to_wCBN.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/third_order/simplified.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Seval.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Deduction/FullNDConsistency.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/Reductions/PCP_to_CFPI.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_enum.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SetConstraints/Reductions/H10UC_SAT_to_FMsetC_SAT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/binZF.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig1.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Reductions/ILL_CLL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL_full_fragment.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Utils/FragmentSyntax.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/InformativeReducibilityFacts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Numbers.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig0.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Util/term_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/wf_chains.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM_dec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Utils/FullSyntax.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_HFD.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Util/Facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/unification/unification.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/iipc2_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FSTD.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/Theories.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/finite.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_elem.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/calculus.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/reductions.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MPM2_HALT_dec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fol_ops.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_REV_dec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_ZFD.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/TM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Util/h10c_utils.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/SBTM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Extract.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/Util/PA2_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/BinSig.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM2_dec.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/KOSBTM/KOSBTM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/ArithLibs/lagrange.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/L_enum.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_string.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/std.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/BPCP_SigBPCP.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCP_to_PCPb.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_ZF.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SeparationLogic/Reductions/MSLSAT_to_SLSAT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/unscoped.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/H10UC_SAT_to_H10UPC_SAT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/SysF.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/Facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Lists/BaseLists.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/bsm_mma.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/binomial.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FST.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPb_iff_BPCP.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Tarski/FullSoundness.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/SemiDecidabilityFacts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/PCP.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/SBTM_enum.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/Util/Subst.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_no_syms.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/AbstractMachines/wCBV.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/DecidabilityFacts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/Facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPb_iff_dPCPb.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_HF.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/bool_list.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/step.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/ars/normalisation.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/ars/basic.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/LClos.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_upto.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_no_self.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_Sig_fin.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/concon/constants.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Base.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Compound/MoveToSymbol.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/focus.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Enumerators/SBTM_HALT_enum.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SeparationLogic/Reductions/FSATdc_to_MSLSAT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/EILL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Prelim.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/CompoundFinTypes.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/membership.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/Util/Tarski.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/ndMM2.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_enum.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/typing.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/IMSELL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/sums.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/encoding.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MMA_pairing.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_nat.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/Facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/discernable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_utils.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN/mm_fractran.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig2_Sign.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/recalg.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/poly_type_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/ars/list_reduction.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/Util/Definitions.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sign_Sig.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_sem_eq.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Single/EncodeTapes.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/enumerable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/H10C.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SeparationLogic/SL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/Util/PA2_categoricity.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/ill_cll.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/L.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig1_1.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/PA2.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/MMA_mon_computable_to_TM_computable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL_friedman.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/compiler_correction.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_rem_syms.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CounterMachines/Reductions/MM2_HALTING_to_CM1_HALT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Deduction/FullND.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/ZF_model.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Util/Enumerable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HilbertCalculi/Reductions/MPCPb_to_HSC_PRV.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/ndMM2.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA_computable_to_MMA_mon_computable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/reln_hfs.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/hfs.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/Enumerable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/deterministic_simulation.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/ZF.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/Signature.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Util/L_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/HaltTM_1_to_SBTM_HALT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Krivine.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN/fractran_utils.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/SemiU.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_ZFeq.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/MPCP_to_MPCPb.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/php.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SeparationLogic/MSL.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/Nat_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/PCP.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/concon/conservativity.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/wCBN.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/MuRec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/CLL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Tarski/FragmentCore.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/countability.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/ZF_conservativity.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/FiniteTarski/DoubleNegation.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMenv/mme_utils.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Util/NaryApp.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/ILL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/FST.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/ArithLibs/luca.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/schellinx.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/MoreEnumerabilityFacts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/Combinators.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_bounded.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/ill_cll_restr.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/SMN.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/interval.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/If.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Reductions/Diophantine_to_MuRec_computable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/SR.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Reductions/LU2SemiU_to_SysF_TYP.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Acceptability.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/HF_model.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_single.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/TRAKHTENBROT_to_FSAT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/CFG.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Compound/WriteString.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/motivation.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/FinNotation.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/H10C_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/eill_mm.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/sorting.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Code/Code.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Reductions/FRACTRAN_computable_to_Diophantine.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/StateWhile.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB/SMX.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Lbeta_nonrefl.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/KOSBTM/KOSBTM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/SSM.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/minFOL_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/Bounded.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/MoreReducibilityFacts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HilbertCalculi/HSC.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/H10Z.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/utils.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Reductions/MM_FRACTRAN.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/prime.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/Eval.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/red_chain_undec_full.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FSAT_direct_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_dec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Reductions/HaltLclosed_to_wCBNclosed.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/fractran_mma.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPb_iff_iPCPb.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Por.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HilbertCalculi/Util/HSCFacts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Reductions/ndMM2_IMSELL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/PCSnf.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/RU2SemiU_to_SemiU.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PolynomialConstraints/LPolyNC.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/third_order/encoding.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_discernable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_godel_beta.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/third_order/pcp.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_definable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_congruence.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/SysF.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Compound/TMTac.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/ill.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/decidable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_dio_poly.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/SequentialComposition.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_noeq.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FOL_intu.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/H10C.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_univ.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/SBTM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_univ_andrej.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/eill.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/BasicDefinitions.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/minimizer.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/typing_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/CSSM_UB_to_SSemiU.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Vec/pos.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/confluence.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Tarski/FragmentFacts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/SMN.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Reflection.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/ill_cll_restr.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_mm.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/FA.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Util/PCP_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/SemiU.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SeparationLogic/SL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Util/prime_seq.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL_minimal.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/wf_incl.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_pctm.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CounterMachines/CM1.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_terms.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/deterministic_simulation.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/CFP.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/reduction.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SetConstraints/FMsetC.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/TM/TMinL/TMinL_extract.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/DiscreteEnumerable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Decidability.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/prim_min.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/binFST.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_cipher.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_defs.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10p_to_FA.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LVector.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_sat_dec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/wf_finite.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Reductions/EILL_ILL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/SSTS.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Tarski/FullCore.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/ListAutomation.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/MuRec/MuRec_extract.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/SSM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Deciders/Halt_REV_FRACTRAN_dec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM/tiles_solvable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Scott.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/dowek/encoding.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/Reductions/PCP_to_CFPP.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/third_order/huet.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/sn_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/EqDec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Lbeta.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/rel_iter.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/While.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_MM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/unification/nth_order_unification.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Util/wCBN_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/FST_model.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HilbertCalculi/Reductions/MPCPb_to_HSC_AX.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_utils_bsm.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/KrivineMclosed_HALT_to_HaltUTM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sign_Sig2.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Reductions/wCBNclosed_to_KrivineMclosed_HALT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Reductions/SysF_TYP_to_SysF_TC.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/EILL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/Asimpl.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB/SMX.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_minZFeq.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_expo.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Prelim/ARS.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/EnumerabilityFacts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_ca.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_k_mma_2_compiler.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/multiplication.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/seteq.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/terms.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/concon/conservativity_constants.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/red_dec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig2_SigSSn1.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMenv/env.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM_2_HALTING_dec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/evaluator.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/Reductions/CFPP_to_CFP.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Deduction/FragmentND.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/imsell.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Compound/Shift.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/iPCPb_to_BSM_HALTING.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FOL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SetConstraints/Util/Facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/PCTM/pctm_sbtm.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/binFOL_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/ComputableTactics.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SeparationLogic/MSL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/DPRM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/Switch.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/Reductions/H10p_to_SOL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/ndMM2/ndmm2_utils.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Tactics/Tactics.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/lists/advanced.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_quotient.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/order.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_comp_strong.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/ComputableTactics.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_rem_cst.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/TM/TMEncoding.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/SBTM_HALT_to_SR.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Lrewrite.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/ArithLibs/matrix.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA2_to_ndMM2_ACCEPT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/unification/systemunification.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_rt_closure.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_comp.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA2_to_MM2.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Computability.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/Aczel.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Util/FRACTRAN_sss.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Dec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/diophantine_equations.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/TM/TMinL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/BSM_computable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_base.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/pure_term_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Utils/FriedmanTranslation.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/MMA_HALTING_n_to_HaltTM_n.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/Aczel_TD.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Tarski/FragmentSoundness.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Util/H10UPC_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/Core.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/ReducibilityFacts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/SBTM_HALT_to_HaltBSM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/SMN_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Models/Aczel_CE.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_recomp.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MM2_to_ndMM2_ACCEPT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/term_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Util/FRACTRAN_computable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/list_bool.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/semantics.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/HaltTM_1_to_PCPb.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Synthetic.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/equivalence.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/quotient.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/crt.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/SyntacticOps.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM/mm_defs.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/H10_to_L.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MM2_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/concon/constants_consequences.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_uniform.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/FRACTRAN_DIO.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/PCTM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/Util/Facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_sig.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/MPCP_to_PCP.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/DepPairs.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/minZF_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Inhabited.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_sat.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/retracts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMenv/mme_defs.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/FiniteTarski/Full.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/ZF_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/wCBN.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Reductions/H10_to_H10p.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/power_decomp.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/godel_coding.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FOL_class.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/Definitions.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/ListEnumerabilityFacts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/SOL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/FiniteTarski/Fragment.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Util/ClosedLAdmissible.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/gfp.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/bpcp.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/PCP_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/SR.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Rice.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/FinTypesDef.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/FRACTRAN_to_H10C_SAT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/Subst.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FST_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/lists/misc.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_simul.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LSum.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig0.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Computable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/H10p.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/compiler.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/syntax.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Util/TM_computable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/InformativeReducibilityFacts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/Models_Equivalent.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_defs.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Code/subcode.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/misc.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MM_to_MMA2.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPX_iff_dPCP.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LProd.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/Definitions.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/lists/basics.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/CFG.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma3_mma2_compiler.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/ReducibilityFacts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LNat.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_decidable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Tarski/FullFacts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/SBTM_HALT_to_HaltTM_1.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MMA_computable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/Infinite.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_binary.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Enumerators/term_enum.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/red_enum.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Lbeta.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/H10_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Krivine.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Fractran/fractran_dio.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_one_rel.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/PCPb_to_HaltL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MM_sss.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/BSM_sss.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/enumerable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/acc_irr.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_REV_dec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Kripke/FragmentCore.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LOptions.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/FiniteTarski/Listability.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PolynomialConstraints/LPolyNC.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/red_utils.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_bij.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_rem_constants.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FST.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MM_computable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Utils/FriedmanTranslationFragment.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CounterMachines/Util/CM1_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM2.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/L.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_eqb.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/EqBool.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Lproc.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Matija/expo_diophantine.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/KOSBTM/HaltTM_1_to_HaltKOSBTM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/TM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_choice.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FOL_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Util/Prelim.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Basic/Mono.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/prelim.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/dowek/reduction.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/NatModel.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_extra.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/bounded_quantification.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/ZF_to_FST.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sign1_Sig.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/FinTypeLookup.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/H10Z_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/Proc.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/binZF_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/iipc2_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/minimizer.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_in.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Reductions/H10_to_MUREC_HALTING.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Tarski/FullSoundness.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Kripke/FragmentSoundness.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_rem_props.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/HaltTM_1_to_MM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HilbertCalculi/HSC.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/SR_to_PCSnf.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/recursor.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/decidable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/SBTM_HALT_to_TSR.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CounterMachines/CM1.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/SR_to_MPCP.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/VectorFin.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Util/Krivine_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/Theories.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB/SMX_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/ars/confluence.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma_simul.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig1.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/measure_ind.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/ars/list_reduction.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Deciders/MM2_UMORTAL_dec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Seval.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/IMSELL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/step.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Util/term_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/CFP.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/bsm_mma.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FSAT_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PolynomialConstraints/Reductions/FMsetC_SAT_to_LPolyNC_SAT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM/bsm_pcp.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/focus.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/TM_to_L.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_string.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MM2_HALTING_to_MM2_ZERO_HALTING.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FSAT_direct_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/acc_irr.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Util/SBTM_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/EqDecDef.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/Reductions/PCP_to_CFPI.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/normalisation.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Util/Facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/wf_chains.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_enum.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/binZF_to_binFST.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_no_syms.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/SMNdl_UB_to_CSSM_UB.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_noeq.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/H10SQC_SAT_to_H10UC_SAT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/HaltTM_1_chain_SemiU.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/PCTM/pctm_defs.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/ILL_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/GenEncode.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/PCSnf.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/InformativeDefinitions.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sign_Sig.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_tac.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_enum.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/wf_incl.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/MuRec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/recomp.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA3_to_MMA2_HALTING.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/ars/evaluator.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Autosubst/unscoped.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/SSTS.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/beta.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Compound/Multi.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_sem_eq.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Enumerators/HaltL_enum.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/Mirror.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig2_Sign.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FOL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Fixpoints.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/TRAKHTENBROT_to_FSAT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/RU2SemiU_to_LU2SemiU.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/list_focus.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Util/Relations.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Ll/ill_cll.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/minFOL_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/ndMM2.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/Vectors.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_upto.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/discernable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Numbers.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Kripke/FragmentToTarski.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/DeductionFacts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Lsimpl.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/deterministic_simulation.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/FinTypes.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/DecidabilityFacts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/ZF.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/BasicFinTypes.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/Undecidability.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fol_ops.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/PA.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/notations.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/List_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/TarskiFacts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/H10.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/focus.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCP_to_PCPb.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/binomial.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SetConstraints/FMsetC.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/ars/basic.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_expo.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/SSemiU_to_RU2SemiU.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/InformativeDefinitions.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Util/h10c_utils.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LFinType.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/typing.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_to_MMA_HALTING.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/unification/higher_order_unification.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/H10C_SAT_to_H10SQC_SAT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Signatures.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/TM/TapeFuns.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Reductions/MM_EILL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/notations.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/axioms.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/MuRec_computable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/mTM_to_TM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Compound/TMTac.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_discrete.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/PA.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/FinNotation.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/H10Z.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/unscoped.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/minZF.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/CompoundFinTypes.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/RU2SemiU_to_SemiU.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/FRACTRAN_to_MMA2.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/FinTypesDef.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM/tiles_solvable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Reductions/Diophantine_to_MuRec_computable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/third_order/simplified.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/ZF.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/ReducibilityFacts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Compound/WriteString.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/Encoding.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/Reductions/H10UC_SAT_to_H10UPC_SAT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/Eval.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/ListAutomation.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/PCP.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_cipher.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Lbeta_nonrefl.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/Util/Definitions.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Single/EncodeTapes.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/interval.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Acceptability.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/Facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/red_utils.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Enumerators/SBTM_HALT_enum.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/Combinators.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/If.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/SemiU_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_godel_beta.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/SysF.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_sig.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Util/NaryApp.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/Robinson.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_basics.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/countability.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/wf_finite.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Code/Code.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/Signature.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/H10C.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMenv/env.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/DiophantineConstraints/H10C_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/utils.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/H10p.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Reductions/H10C_SAT_to_RA_UNIV_HALT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/ZF_to_HF.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/Reductions/CFPI_to_CFI.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/EILL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/Facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/fin_dec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/SemiU.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/reductions.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/EqDec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Por.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/FSATd_to_FSATdc.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/H10UPC_to_FOL_minimal.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/confluence.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Reductions/MM_FRACTRAN.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/TM/TMEncoding.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/MoreEnumerabilityFacts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/BasicDefinitions.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/PCTM_HALT_to_BSM_HALTING.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Tarski/FragmentSoundness.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LVector.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Lproc.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Reductions/EILL_CLL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HilbertCalculi/Util/HSCFacts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/prim_min.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/PCPb_to_FOL_intu.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Dio/dio_rt_closure.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Tactics/Tactics.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/PA2.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/fo_sat.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Scott.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/Lsimpl.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM2_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/FRACTRAN_DIO.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/iPCPb_to_BSM_HALTING.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Tarski/FragmentCore.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/MuRec/MuRec_extract.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/HaltL_to_HaltLclosed.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Inhabited.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/PCPb_to_MM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LNat.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM2_dec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FOL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/PCP_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/SysF_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/PCTM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/H10_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/ILL_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/MuRec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/MoreReducibilityFacts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/HaltTM_1_chain_SemiU.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Reductions/FRACTRAN_computable_to_Diophantine.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/EqDecDef.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Decidability.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FST_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Util/pure_term_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Dec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MM_to_MMA2.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/MPCP_to_MPCPb.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Reductions/SysF_TYP_to_SysF_TC.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/Reductions/PCP_to_CFPP.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Util/Diophantine.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/KrivineMclosed_HALT_to_HaltUTM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MUREC_MM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/PA_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/IMSELL_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/HaltL_to_HaltTM_5.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/TM/TMinL/TMinL_extract.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Reductions/HaltTM_1_to_SysF_TYP.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPb_iff_iPCPb.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Deduction/FragmentNDConsistency.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/bpcp.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/ndMM2/ndmm2_utils.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Reductions/wCBNclosed_to_KrivineMclosed_HALT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Tarski/FullCore.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/third_order/pcp.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Deduction/FullND.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/wCBN_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/Definitions.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/HaltTM_1_to_PCPb.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/Equality.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Reductions/HaltTM_1_to_SysF_INH.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/binZF.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/SBTM_HALT_to_PCTM_HALT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/Undecidability.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Util/wCBN_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Computability.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Reductions/H10C_SAT_to_RA_UNIV_HALT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Util/FRACTRAN_sss.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_fold.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/binFST_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/NatModel.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Reductions/ILL_CLL.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LBool.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Reductions/wCBNclosed_to_wCBN.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Reductions/MM_computable_to_FRACTRAN_computable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CounterMachines/Reductions/HaltTM_1_to_CM1_HALT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/FiniteTarski/Listability.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/SBTM_to_MMA2_HALTING.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/red_enum.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/FiniteTarski/Full.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/SMN.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HilbertCalculi/HSC.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LOptions.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/TRAKHTENBROT/Sig_discrete.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/SSM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Deduction/FullNDConsistency.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Combinators/SequentialComposition.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/SBTM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Reductions/HaltTM_1_to_FRACTRAN_HALTING.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/SBTM_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FSAT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/evaluator.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LSum.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/BSM_computable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Reductions/H10_to_H10p.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils_string.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/UTM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_HALTING_to_MM2_HALTING.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/FRACTRAN_to_MMA2.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Util/Enumerable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/FiniteTarski/Fragment.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PolynomialConstraints/LPolyNC.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/HaltTM_1_to_SemiU.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/Enumerable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Reductions/iBPCP_MM.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/concon/constants_consequences.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_MM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA2_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HilbertCalculi/HSC_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/FST.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SetConstraints/FMsetC.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/SemiDecidabilityFacts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/list_focus.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/concon/conservativity_consequences.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Krivine_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SetConstraints/Util/Facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/SemiU_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Util/TM_computable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/Nat_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA/mma3_mma2_compiler.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/TM/TMinL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Util/FRACTRAN_computable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/TM_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/L_computable_to_TM_computable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/lists/misc.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LProd.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/recursor.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Deduction/FragmentND.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/PA2_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/TM/TapeFuns.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPb_iff_BPCP.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Wf/acc_irr.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA2_to_MMA2_zero.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FOL_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/Proc.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_nat.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/ra_simul.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/wCBN.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Reductions/H10_to_MUREC_HALTING.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/SR_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/FA.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/KOSBTM/KOSBTM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SeparationLogic/SL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM2_dec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/binZF_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPb_iff_dPCPb.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/goldfarb/motivation.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/RA_UNIV_HALT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/retracts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Reductions/EILL_ILL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_eqb.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPX_iff_dPCP.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Krivine.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/MMA_computable_to_TM_computable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/VectorFin.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/HaltTM_1_to_CSSM_UB.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CounterMachines/CM1.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/CFG_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/L.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/CFG.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/Models_Equivalent.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/tactics.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/RA_UNIV_HALT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/Util/Facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/CM1_HALT_to_SMNdl_UB/SMX.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/SOL_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_in.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Semantics/Kripke/FragmentToTarski.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/BinSig.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Reductions/MM_EILL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/beta.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/HaltTM_1_to_MM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MUREC_MM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/CFP_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/tactics.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SeparationLogic/MSL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/std.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Vectors/Vectors.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Tactics/Tactics.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/binFST.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/misc.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/HaltTM_1_to_PCP.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM2_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/InformativeReducibilityFacts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/HaltTM_1_to_iPCPb.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/H10.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FSAT_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/second_order/diophantine_equations.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Sets/Signatures.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/ars/normalisation.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MMA_computable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/IMSELL_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/DepPairs.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SeparationLogic/Reductions/MSLSAT_to_SLSAT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FST.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/EqBool.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LBool.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/binFOL_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Lists/BaseLists.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/SSTS.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/SR.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/SysF_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Enumerators/term_enum.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Compound/Multi.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/PCPb_to_MM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/ndMM2/ndmm2_utils.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA3_to_MMA2_HALTING.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Reductions/iBPCP_MM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/SBTM_to_MMA2_HALTING.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/Ackermann.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/BasicFinTypes.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LFinType.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HilbertCalculi/HSC_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/ZF_to_HF.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/FinTypeLookup.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/CLL_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/PA.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes/FinTypesDef.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/PCTM_HALT_to_BSM_HALTING.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PolynomialConstraints/LPolyNC_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_to_MMA_HALTING.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/Encoding.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/UTM.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/FSAT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/TM_to_L.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/MuRec_computable_to_L_computable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MMA2_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_enc.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/RA_UNIV_HALT_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Reductions/FSATd_to_FSATdc.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/CLL_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/HaltTM_1_to_SR.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SetConstraints/FMsetC_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_extra.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Reductions/HaltTM_1_to_SysF_TC.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Util/MM_computable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/ndMM2_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/wCBN_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/SBTM_HALT_to_PCTM_HALT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/SSTS_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CounterMachines/CM1_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/CFP.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Deduction/FragmentNDConsistency.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/MMA2_to_MMA2_zero.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/H10p.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/L_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Enumerators/HaltL_enum.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/SSM_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Reductions/HaltTM_1_to_SysF_TYP.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/UTM_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/PCSnf_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_basics.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Reductions/EILL_CLL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/SMN_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM/tiles_solvable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Krivine_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/ndMM2_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Reductions/HaltTM_1_to_SysF_INH.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SeparationLogic/SL_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/MuRec_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Computability/Fixpoints.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/PCSnf.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/RU2SemiU_to_SemiU.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SeparationLogic/MSL_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/ILL/Reductions/ILL_CLL.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Deduction/FullNDConsistency.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/LambdaCalculus/Reductions/wCBNclosed_to_wCBN.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/Equality.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/H10p_undec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/PA_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SemiUnification/Reductions/HaltTM_1_to_SemiU.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/BSM_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/axioms.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM_dec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CounterMachines/Reductions/HaltTM_1_to_CM1_HALT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/Reductions/HaltTM_1_to_FRACTRAN_HALTING.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/reductions.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/MuRec_computable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN_dec.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/SBTM_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CounterMachines/CM1_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Utils/FragmentSyntax.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LTerm.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/binFST_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FRACTRAN/FRACTRAN_dec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/Reductions/BSM_HALTING_to_MM2_HALTING.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/HaltL_to_HaltTM_5.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Numbers.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SetConstraints/FMsetC_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PolynomialConstraints/LPolyNC_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_fold.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/Reductions/CFPI_to_CFI.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/TM_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/SMN_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Reductions/HaltTM_1_to_CSSM_UB.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/finite.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/SSM_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/EqDecDef.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/SBTM_enum.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/SR_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/HaltL_to_HaltLclosed.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/calculus.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/CFG_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/CFG/CFP_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/HaltTM_1_to_PCP.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/PA.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SystemF/Reductions/HaltTM_1_to_SysF_TC.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/HaltTM_1_to_iPCPb.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/L_enum.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StackMachines/Util/Facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/PA2_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MinskyMachines/MM_dec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/Util/RA_UNIV_HALT_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPb_iff_BPCP.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/axioms.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LTerm.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/InformativeDefinitions.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/finite.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Prelim.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Utils/FullSyntax.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SOL/SOL_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_enc.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/List/List_nat.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Prelim.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/L_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/Reductions/HaltTM_1_to_SR.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/std.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/concon/conservativity_consequences.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/L_computable_to_TM_computable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/Util/Diophantine.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/Lists.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/SSTS_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/DLW/Utils/utils.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Arithmetics/Robinson.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Synthetic/SemiDecidabilityFacts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/StringRewriting/PCSnf_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/Reductions/MMA_computable_to_TM_computable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/LTactics.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/Ackermann.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Lists/BaseLists.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/H10/H10p_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/MuRec/MuRec_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/UTM_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/Subst.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/BinSig.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/PCP/Reductions/PCPb_iff_dPCPb.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Utils/FragmentSyntax.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/std/ars/normalisation.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/Facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SeparationLogic/MSL_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LUnit.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Base.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/TM/SBTM_enum.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Reductions/MuRec_computable_to_L_computable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/unification/unification.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/LUnit.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/SeparationLogic/SL_undec.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/L_enum.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/Base.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Functions/Subst.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/calculus/calculus.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Tactics/LTactics.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Utils/FullSyntax.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/Shared/Libs/PSL/FiniteTypes.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/L/Datatypes/Lists.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/HOU/unification/unification.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Undecidability/FOL/Syntax/Facts.vopam remove -y coq-library-undecidability.1.1+8.17