| d74b5ce | Yannick Forster | 04 August 2020, 11:09:50 UTC | update README, trigger travis | 04 August 2020, 11:09:50 UTC |
| 5581a0e | Yannick Forster | 04 August 2020, 10:10:50 UTC | Fix opam and travis file | 04 August 2020, 10:10:50 UTC |
| b75857d | Yannick Forster | 04 August 2020, 09:40:11 UTC | Fix warning "Declaring arbitrary terms as hints is fragile" | 04 August 2020, 09:40:11 UTC |
| 8057818 | Yannick Forster | 04 August 2020, 09:24:16 UTC | Delete .#utils_list.v | 04 August 2020, 09:24:16 UTC |
| 588e33f | Yannick Forster | 04 August 2020, 08:26:03 UTC | Fkx last admit | 04 August 2020, 08:26:03 UTC |
| fd0801d | Yannick Forster | 04 August 2020, 07:43:25 UTC | Remove two more admits | 04 August 2020, 07:43:25 UTC |
| 77d9d59 | Yannick Forster | 04 August 2020, 07:37:18 UTC | Close some admits: lia does not run subst on variables `z := ...` anymore | 04 August 2020, 07:37:18 UTC |
| 2e56973 | Yannick Forster | 04 August 2020, 06:59:11 UTC | Remove commented out code containing admits, `git grep admit` returns no false positives anymore | 04 August 2020, 06:59:11 UTC |
| cb8458a | Yannick Forster | 04 August 2020, 06:57:08 UTC | Finish porting to 8.12 | 04 August 2020, 06:57:08 UTC |
| 65e4b26 | Yannick Forster | 03 August 2020, 16:19:52 UTC | Progress porting to 8.12 | 03 August 2020, 16:19:52 UTC |
| 2d64ced | Yannick Forster | 03 August 2020, 15:31:19 UTC | "Run TemplateProgram" is now "MetaCoq Run" | 03 August 2020, 15:31:19 UTC |
| 57e3631 | Yannick Forster | 03 August 2020, 15:30:45 UTC | Various fixes | 03 August 2020, 15:30:45 UTC |
| 9194b17 | Yannick Forster | 03 August 2020, 14:01:21 UTC | Fix "Warning: Notation leb is deprecated since 8.12. Use Bool.le instead." | 03 August 2020, 15:00:42 UTC |
| 43acd2e | Yannick Forster | 03 August 2020, 13:54:33 UTC | Merge pull request #58 from DmxLarchey/remove_prelim Removing Shared.Prelim where I know how to ... | 03 August 2020, 13:54:33 UTC |
| f4e599c | Yannick Forster | 03 August 2020, 05:45:10 UTC | Merge pull request #59 from yforster/reorg_TM Reorganising TM | 03 August 2020, 05:45:10 UTC |
| 3db576b | Fabian Kunze | 01 August 2020, 01:09:57 UTC | Merge pull request #1 from lgaeher/coq-8.11 Merge TM to SAT part of Cook proof + Clique reduction + ... | 01 August 2020, 01:09:57 UTC |
| 8c47b45 | Fabian Kunze | 01 August 2020, 01:00:43 UTC | -Added CookLevin.v containing final lemma Merge branch 'coq-8.11' of github.com:lgaeher/coq-computability-complexity into coq-8.11-for-merge | 01 August 2020, 01:00:43 UTC |
| 84d067c | Fabian Kunze | 01 August 2020, 00:03:46 UTC | -improved Performance of Tm to TPR reduction by: *adding many manual inversion lemmas *adding "par:" selector for parallel ltac evaluation *added many "abstract" tacticals for work-heavy parts (does this save time? not sure) -also Merge branch 'coq-8.11' of github.com:lgaeher/coq-computability-complexity into coq-8.11-for-merge | 01 August 2020, 00:03:46 UTC |
| 0073adc | Lennard Gäher | 31 July 2020, 20:22:47 UTC | whoops, forgot to git add CoqProject | 31 July 2020, 20:22:47 UTC |
| fa56117 | Lennard Gäher | 31 July 2020, 20:21:38 UTC | move files to CookPrelim | 31 July 2020, 20:21:38 UTC |
| b7e1835 | Lennard Gäher | 31 July 2020, 20:03:57 UTC | remove won't-fix lemma in overview | 31 July 2020, 20:03:57 UTC |
| 9973368 | Lennard Gäher | 31 July 2020, 20:03:18 UTC | fix admitted stuff in TMflatComp | 31 July 2020, 20:03:18 UTC |
| daa7f9f | Yannick Forster | 31 July 2020, 17:16:50 UTC | Add L_undec file | 31 July 2020, 17:16:50 UTC |
| 3144080 | Yannick Forster | 31 July 2020, 16:23:07 UTC | No omega, better L | 31 July 2020, 16:23:22 UTC |
| 7926ebc | Yannick Forster | 31 July 2020, 12:36:12 UTC | rename mTM to TM | 31 July 2020, 12:36:12 UTC |
| 6fd86ae | Yannick Forster | 31 July 2020, 11:56:17 UTC | Remove TM/tape.v | 31 July 2020, 11:56:17 UTC |
| 9126ce1 | Yannick Forster | 31 July 2020, 11:56:05 UTC | Merge branch 'reorg_TM' of github.com:yforster/coq-library-undecidability into reorg_TM | 31 July 2020, 11:56:05 UTC |
| ad7aa23 | Yannick Forster | 31 July 2020, 08:57:05 UTC | everything compiles | 31 July 2020, 08:57:05 UTC |
| b8d4bfe | Dominique Larchey-Wendling | 31 July 2020, 08:28:01 UTC | some ideas for axiomatized tapes | 31 July 2020, 08:28:01 UTC |
| ea335c1 | Fabian Kunze | 31 July 2020, 08:27:43 UTC | small tweaks to maybe speed up TM-to-TPR-reduction by decrasing backtracking | 31 July 2020, 08:27:43 UTC |
| 86c90b8 | Fabian Kunze | 31 July 2020, 08:27:12 UTC | Additions for Cook-Levin Theorem | 31 July 2020, 08:27:12 UTC |
| 5e28fd9 | Yannick Forster | 31 July 2020, 07:44:59 UTC | Rename moves, start commenting TM.v | 31 July 2020, 08:08:41 UTC |
| 0e8321f | Dominique Larchey-Wendling | 30 July 2020, 22:12:37 UTC | correction my own typos | 30 July 2020, 22:12:37 UTC |
| 9872172 | Dominique Larchey-Wendling | 30 July 2020, 22:07:46 UTC | trying a comments only commit | 30 July 2020, 22:07:46 UTC |
| 6c40be2 | Lennard Gäher | 30 July 2020, 21:08:04 UTC | remove LLNat + LLists + merge into other files; fix compilation; TODOs: two admitteds in L/TM/TMFlatComp; overview.v | 30 July 2020, 21:08:04 UTC |
| 42b009f | Yannick Forster | 30 July 2020, 16:45:27 UTC | add moved files | 30 July 2020, 16:45:27 UTC |
| b5a4da1 | Yannick Forster | 30 July 2020, 16:45:17 UTC | finish first part | 30 July 2020, 16:45:17 UTC |
| 40b36c3 | Yannick Forster | 30 July 2020, 14:18:34 UTC | Move problems | 30 July 2020, 15:14:00 UTC |
| c85dc60 | Yannick Forster | 30 July 2020, 14:07:26 UTC | intermediate commit | 30 July 2020, 14:07:59 UTC |
| 7f88d8e | Dominique Larchey-Wendling | 30 July 2020, 12:39:14 UTC | removing Shared.Prelim where I know how to ... | 30 July 2020, 12:39:14 UTC |
| bfa7788 | Yannick Forster | 30 July 2020, 06:03:56 UTC | Merge pull request #57 from DmxLarchey/omega_to_lia Replace Omega by Lia (in many places but not everywhere ...) | 30 July 2020, 06:03:56 UTC |
| 0376138 | Dominique Larchey-Wendling | 29 July 2020, 22:49:11 UTC | no more omega in Shared/Libs/DLW | 29 July 2020, 22:49:11 UTC |
| cb685f3 | Dominique Larchey-Wendling | 29 July 2020, 21:12:22 UTC | No more omega in H10 | 29 July 2020, 21:12:22 UTC |
| f5b28d1 | Dominique Larchey-Wendling | 29 July 2020, 20:21:41 UTC | No more Omega in MuREC | 29 July 2020, 20:21:41 UTC |
| d09a948 | Dominique Larchey-Wendling | 29 July 2020, 19:46:47 UTC | No more Omega in ILL | 29 July 2020, 19:46:47 UTC |
| 35d7077 | Dominique Larchey-Wendling | 29 July 2020, 19:37:40 UTC | No more Omega in Fractran | 29 July 2020, 19:37:40 UTC |
| 5eff4d5 | Dominique Larchey-Wendling | 29 July 2020, 19:19:40 UTC | no omega anymore in MinskyMachines/ | 29 July 2020, 19:19:40 UTC |
| a527c2d | Dominique Larchey-Wendling | 29 July 2020, 18:50:18 UTC | Merge pull request #56 from DmxLarchey/move_bsm BinaryStackMachines to StackMachines | 29 July 2020, 18:50:18 UTC |
| b0a6c6d | Dominique Larchey-Wendling | 29 July 2020, 13:00:23 UTC | cleanup the _CoqProject | 29 July 2020, 13:00:23 UTC |
| 849eca7 | Dominique Larchey-Wendling | 29 July 2020, 12:27:30 UTC | migration BSM from BinaryStackMachines to StackMachines + omega -> lia (partial) migration | 29 July 2020, 12:27:30 UTC |
| 3b103df | Yannick Forster | 29 July 2020, 08:16:27 UTC | Merge pull request #54 from DmxLarchey/reorg_machines Restructured Minsky machines, Binary Stack machines and FRACTRAN | 29 July 2020, 08:16:27 UTC |
| 6db6be1 | Dominique Larchey-Wendling | 28 July 2020, 19:49:47 UTC | new more robust tactics reduce with chain ... undec from ... using chain ... | 28 July 2020, 19:49:47 UTC |
| 8c06b2b | Dominique Larchey-Wendling | 28 July 2020, 16:40:58 UTC | added M. Wuttke's nice trick for typing reduction chains | 28 July 2020, 16:40:58 UTC |
| 2d27356 | Dominique Larchey-Wendling | 28 July 2020, 12:41:58 UTC | renamed iBPCP_BSM | 28 July 2020, 12:41:58 UTC |
| f22adc6 | Dominique Larchey-Wendling | 28 July 2020, 10:49:24 UTC | documented sss notations removed omega | 28 July 2020, 10:49:24 UTC |
| 202001f | Dominique Larchey-Wendling | 28 July 2020, 09:55:00 UTC | Merge branch 'reorg_machines' into reorg_2 with some duplicate files moved or removed | 28 July 2020, 09:55:00 UTC |
| 0a101e9 | Dominique Larchey-Wendling | 28 July 2020, 09:01:32 UTC | Merge remote-tracking branch 'upstream/coq-8.11' into coq-8.11 | 28 July 2020, 09:01:32 UTC |
| d3770ee | Yannick Forster | 28 July 2020, 07:18:44 UTC | Merge pull request #53 from mrhaandi/dep_clean singleTM and string rewriting dependencies cleanup | 28 July 2020, 07:18:44 UTC |
| b33f610 | Yannick Forster | 28 July 2020, 06:38:02 UTC | Merge pull request #55 from uds-psl/delete-count-states-haskell Delete countStates.hs | 28 July 2020, 06:38:02 UTC |
| c36c6e9 | Dominique Larchey-Wendling | 28 July 2020, 06:35:19 UTC | forgot the files ... | 28 July 2020, 06:35:19 UTC |
| 0fdc7ca | Dominique Larchey-Wendling | 28 July 2020, 06:34:05 UTC | added undec for halting of MMA2/MM2 on the 0 state via the generic compiler ;-) | 28 July 2020, 06:34:05 UTC |
| 4f5c681 | Dominique Larchey-Wendling | 27 July 2020, 04:53:08 UTC | restructured H10(Z) for conformity | 27 July 2020, 04:53:08 UTC |
| 87d9fed | Dominique Larchey-Wendling | 27 July 2020, 04:08:00 UTC | cleanup in ILL ~~> conformity with guidelines | 27 July 2020, 04:08:00 UTC |
| ec73001 | Dominique Larchey-Wendling | 26 July 2020, 01:14:53 UTC | Merge pull request #12 from DmxLarchey/reorg_in_transit Reoganised according to the new guidelines | 26 July 2020, 01:14:53 UTC |
| 48b0420 | Dominique Larchey-Wendling | 26 July 2020, 01:00:21 UTC | reorganised with new structure BinaryStackMachines MinskyMachines FRACTRAN and put reductions ending there in the corresponding directory | 26 July 2020, 01:00:21 UTC |
| 0307af0 | Dominique Larchey-Wendling | 24 July 2020, 13:45:01 UTC | transition to mandatory structure | 24 July 2020, 13:45:01 UTC |
| af880f5 | Fabian Kunze | 24 July 2020, 09:52:59 UTC | -added install script instructions for dependencies -adjusted TMGenNP_fixed_singleTapeTM_to_FlatFunSingleTMGenNP to be slightly more general, allowing it to connect to the other halve of the proof | 24 July 2020, 09:52:59 UTC |
| 099a5ad | mrhaandi | 24 July 2020, 09:35:56 UTC | added Hilberts_Tenth theorem | 24 July 2020, 09:35:56 UTC |
| d575616 | Yannick Forster | 24 July 2020, 05:00:50 UTC | Delete countStates.hs | 24 July 2020, 05:00:50 UTC |
| 20a3c34 | Dominique Larchey-Wendling | 23 July 2020, 23:07:02 UTC | update of a comment | 23 July 2020, 23:07:02 UTC |
| 24ad0f0 | Dominique Larchey-Wendling | 23 July 2020, 22:50:31 UTC | the README was ok ... just small ups | 23 July 2020, 22:50:31 UTC |
| 166c490 | Dominique Larchey-Wendling | 23 July 2020, 21:48:01 UTC | moved the MinskyMachines, BinaryStackMachines and FRACTRAN to top-level moved the Code compiler (CPP19) to Shared/Libs/DLW | 23 July 2020, 21:48:01 UTC |
| 8d6e95b | Lennard Gäher | 23 July 2020, 21:46:05 UTC | remove experimental UpToCNary poly file | 23 July 2020, 21:46:05 UTC |
| 533d505 | Lennard Gäher | 23 July 2020, 21:43:22 UTC | restore website gitignore | 23 July 2020, 21:43:22 UTC |
| 85c6ab8 | Lennard Gäher | 23 July 2020, 19:45:23 UTC | remove website config | 23 July 2020, 19:45:23 UTC |
| 57578cd | Lennard Gäher | 23 July 2020, 19:41:06 UTC | restore README.md to original | 23 July 2020, 19:41:06 UTC |
| 943cbd0 | Lennard Gäher | 23 July 2020, 19:40:19 UTC | remove website stuff | 23 July 2020, 19:40:19 UTC |
| d4d20c9 | Lennard Gäher | 23 July 2020, 19:38:39 UTC | remove tex stuff, SharpP | 23 July 2020, 19:38:39 UTC |
| f651de5 | Lennard Gäher | 23 July 2020, 17:50:44 UTC | fix all admitted goals that arose when porting | 23 July 2020, 17:50:44 UTC |
| 5e66486 | Lennard Gäher | 23 July 2020, 15:26:59 UTC | fix compilation under 8.11 | 23 July 2020, 15:27:19 UTC |
| 1b3691a | Lennard Gäher | 22 July 2020, 15:53:56 UTC | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.11-2 | 22 July 2020, 15:53:56 UTC |
| bdf27d5 | Lennard Gäher | 22 July 2020, 15:43:44 UTC | continue work on port to 8.11 | 22 July 2020, 15:43:44 UTC |
| ac848af | Lennard Gäher | 22 July 2020, 15:42:38 UTC | minor fix to make leq_crossout work again | 22 July 2020, 15:42:38 UTC |
| 948e0fe | Fabian Kunze | 22 July 2020, 14:44:56 UTC | small tweaks | 22 July 2020, 14:44:56 UTC |
| f8d7c7d | Fabian Kunze | 22 July 2020, 10:57:25 UTC | Updated to new, ocally installed metacoq (see install.txt), allowing use of qualified names in extraction. Alsu added missing file | 22 July 2020, 10:57:25 UTC |
| 6292782 | Fabian Kunze | 20 July 2020, 14:38:26 UTC | tidies up a bit | 20 July 2020, 14:38:26 UTC |
| f3afc7d | Dominique Larchey-Wendling | 19 July 2020, 07:52:07 UTC | Merge remote-tracking branch 'upstream/coq-8.11' into coq-8.11 | 19 July 2020, 07:52:07 UTC |
| 56bcde7 | mrhaandi | 17 July 2020, 11:06:05 UTC | added many-one reductions for semi-unification cleaned up singleTM dependencies cleans up string rewriting dependencies added functional two-counter machines | 17 July 2020, 11:06:05 UTC |
| 9ae49c1 | Fabian Kunze | 15 July 2020, 12:17:13 UTC | finished reduction from gen-NP to gen-TM Left: small discrepancy in how the TM-alphabet is encoded | 15 July 2020, 12:57:00 UTC |
| 389e85e | Fabian Kunze | 08 July 2020, 13:43:15 UTC | continuation polyTimeComputability | 08 July 2020, 13:43:15 UTC |
| c98163e | Yannick Forster | 30 June 2020, 13:59:35 UTC | Merge pull request #52 from mrhaandi/SemiUnification Semi-unification (and more) | 30 June 2020, 13:59:35 UTC |
| 3d981f8 | Andrej Dudenhefner | 28 June 2020, 18:05:44 UTC | added undecidability of semi-unification added undecidability of uniform H10 constraint solvability added undecidability of one counter machine halting added undecidability of problems for Hilbert-calculi added undecidability of linear polynomial constraint solvability added undecidability of finite multiset constraint solvability | 28 June 2020, 18:05:44 UTC |
| 32c934d | Yannick Forster | 26 June 2020, 12:12:08 UTC | Merge pull request #50 from yforster/SyntheticDir New central Synthetic.Definitions file | 26 June 2020, 12:12:08 UTC |
| 3e3b665 | Fabian Kunze | 08 June 2020, 09:59:28 UTC | Finished non-computability-related part of LM to mTM reduction | 08 June 2020, 10:01:26 UTC |
| a9f3939 | Lennard Gäher | 06 June 2020, 21:36:45 UTC | Merge branch 'master' into coq-8.11-2 | 06 June 2020, 21:37:43 UTC |
| 0436312 | Lennard Gäher | 06 June 2020, 21:31:01 UTC | track changes | 06 June 2020, 21:31:01 UTC |
| f95e2be | Fabian Kunze | 04 June 2020, 13:05:18 UTC | WIP on LM to TM for closing Cook-Theorem-Assumptions | 04 June 2020, 13:05:18 UTC |
| 28e91e3 | Fabian Kunze | 26 May 2020, 10:28:32 UTC | -fixed "halt-or-diverge" definition for TMs -worked on LM->TM lemma | 26 May 2020, 10:28:32 UTC |
| 13f5bf7 | Fabian Kunze | 26 May 2020, 08:06:52 UTC | Completed construction of TM tfor LM->TM reduction | 26 May 2020, 08:06:52 UTC |
| d571df2 | Fabian Kunze | 08 May 2020, 10:47:23 UTC | finished size-analysis of LM-interpreter | 08 May 2020, 10:47:23 UTC |
