| 269699c | Yannick Forster | 26 January 2023, 17:27:59 UTC | Merge pull request #190 from JoJoDeveloping/coq-8.16 Remove dependency on Synthetic.Undecidability for non-_undec files | 26 January 2023, 17:27:59 UTC |
| a2e1b96 | Yannick Forster | 26 January 2023, 15:40:47 UTC | Merge pull request #189 from dominik-kirst/fol-library-mr Closes https://github.com/uds-psl/coq-library-undecidability/issues/177 | 26 January 2023, 15:40:47 UTC |
| 300f0b1 | Johannes Hostert | 26 January 2023, 14:11:21 UTC | Remove no longer necessary README.md | 26 January 2023, 14:11:21 UTC |
| 79a2388 | Johannes Hostert | 26 January 2023, 05:46:22 UTC | Add some files necessary for FOL | 26 January 2023, 13:52:56 UTC |
| f977e47 | Johannes Hostert | 16 January 2023, 21:21:41 UTC | Address reviews | 16 January 2023, 21:21:41 UTC |
| abcbc7f | Johannes Hostert | 11 January 2023, 22:21:22 UTC | Make renaming consistent | 11 January 2023, 22:21:38 UTC |
| 123e47c | Johannes Hostert | 11 January 2023, 22:02:15 UTC | rename red_undec.v in TRAKHTENBROT as it does not actually collect undec files | 11 January 2023, 22:02:15 UTC |
| 128bbbf | Johannes Hostert | 11 January 2023, 21:55:46 UTC | Remove dependency on Synthetic.Undecidability for non-_undec files | 11 January 2023, 21:55:46 UTC |
| 82f0997 | Johannes Hostert | 11 January 2023, 21:25:44 UTC | Remove spurious imports of Undecidability.Synthetic.Undecidability in FOL | 11 January 2023, 21:26:06 UTC |
| a29ffa2 | Johannes Hostert | 11 January 2023, 13:57:41 UTC | Remove FOLP | 11 January 2023, 13:57:41 UTC |
| 4715d8f | Johannes Hostert | 05 January 2023, 02:08:17 UTC | Remove commented-out code in FOL | 05 January 2023, 02:08:17 UTC |
| cfc2d60 | Johannes Hostert | 05 January 2023, 01:33:45 UTC | Actually perform aforementioned merge | 05 January 2023, 01:33:45 UTC |
| 6731dde | Johannes Hostert | 04 January 2023, 15:05:49 UTC | Merge branch 'fol-library-split' into HEAD | 04 January 2023, 15:05:49 UTC |
| 646043f | Johannes Hostert | 04 January 2023, 12:52:08 UTC | Retain just CLUP | 04 January 2023, 12:52:08 UTC |
| 48be386 | Johannes Hostert | 04 January 2023, 12:49:02 UTC | Final state before FOL split | 04 January 2023, 12:49:02 UTC |
| ffe298d | Johannes Hostert | 03 January 2023, 13:23:10 UTC | Split project | 03 January 2023, 13:28:12 UTC |
| 0513e0a | Johannes Hostert | 03 January 2023, 12:03:25 UTC | Move non-undec things to separate folders | 03 January 2023, 12:03:25 UTC |
| 3e32e54 | Johannes Hostert | 02 January 2023, 15:28:45 UTC | Finish renaming | 02 January 2023, 15:28:45 UTC |
| e0c024c | Johannes Hostert | 02 January 2023, 14:53:05 UTC | Tennenbaum2 => Tennenbaum | 02 January 2023, 14:53:05 UTC |
| b1ff754 | Andrej Dudenhefner | 21 December 2022, 22:15:05 UTC | Merge pull request #188 from mrhaandi/less-TM-tapemagic more robust TM proofs | 21 December 2022, 22:15:05 UTC |
| d3edc67 | Andrej Dudenhefner | 20 December 2022, 12:00:02 UTC | more robust TM proofs | 21 December 2022, 11:16:08 UTC |
| 92af8ae | Johannes Hostert | 13 December 2022, 04:29:29 UTC | Oh Tennenbaum | 13 December 2022, 04:29:29 UTC |
| 61009e1 | Andrej Dudenhefner | 08 December 2022, 13:29:13 UTC | Merge pull request #187 from mrhaandi/faster-MuRec faster MuRec extraction | 08 December 2022, 13:29:13 UTC |
| 01b6566 | Andrej Dudenhefner | 08 December 2022, 12:36:13 UTC | faster MuRec extraction | 08 December 2022, 12:36:13 UTC |
| 438d74d | Andrej Dudenhefner | 07 December 2022, 11:14:50 UTC | Merge pull request #186 from mrhaandi/faster-SOL faster SOL, TM_to_BSM | 07 December 2022, 11:14:50 UTC |
| 41e6da1 | Andrej Dudenhefner | 06 December 2022, 14:12:41 UTC | faster SOL, TM_to_BSM | 07 December 2022, 10:27:39 UTC |
| 0bc699e | Andrej Dudenhefner | 02 December 2022, 17:46:12 UTC | Merge pull request #185 from mrhaandi/less-shared reduced Shared usage and global side effects | 02 December 2022, 17:46:12 UTC |
| ccb50ca | Andrej Dudenhefner | 30 November 2022, 10:03:00 UTC | reduced Shared usage and global side effects | 02 December 2022, 16:37:21 UTC |
| 240b68c | Andrej Dudenhefner | 25 November 2022, 14:50:50 UTC | Merge pull request #184 from mrhaandi/warnings-8.17 removed many 8.17 warnings | 25 November 2022, 14:50:50 UTC |
| 36e90e1 | Andrej Dudenhefner | 25 November 2022, 14:34:59 UTC | faster TM to BSM | 25 November 2022, 14:37:14 UTC |
| 24bc942 | Andrej Dudenhefner | 23 November 2022, 13:44:44 UTC | removed many 8.17 warnings faster, more stable HOU | 25 November 2022, 14:36:46 UTC |
| 6abaebc | Andrej Dudenhefner | 15 November 2022, 15:52:47 UTC | Merge pull request #183 from mrhaandi/robust-TM more robust TM | 15 November 2022, 15:52:47 UTC |
| 13600b8 | Andrej Dudenhefner | 10 November 2022, 14:52:41 UTC | more robust TM - better goal management - less deprecated tactics - less dead code - no Equations package | 15 November 2022, 15:35:28 UTC |
| 12e9dd9 | Andrej Dudenhefner | 10 November 2022, 12:20:10 UTC | Merge pull request #182 from mrhaandi/less-ListAutomation less Shared.ListAutomation | 10 November 2022, 12:20:10 UTC |
| 55578a4 | Andrej Dudenhefner | 10 November 2022, 12:02:47 UTC | less Shared.ListAutomation | 10 November 2022, 12:02:47 UTC |
| 2e5de03 | Yannick Forster | 09 November 2022, 14:19:09 UTC | Merge pull request #181 from uds-psl/yforster-patch-2 | 09 November 2022, 14:19:09 UTC |
| cb8d4bf | Yannick Forster | 09 November 2022, 14:18:50 UTC | Merge branch 'coq-8.16' into yforster-patch-2 | 09 November 2022, 14:18:50 UTC |
| 7445301 | Yannick Forster | 09 November 2022, 14:09:32 UTC | Merge pull request #180 from DmxLarchey/murec_eq_dec | 09 November 2022, 14:09:32 UTC |
| 4210632 | Yannick Forster | 09 November 2022, 14:09:15 UTC | Merge pull request #176 from mrhaandi/L-MMA-computable | 09 November 2022, 14:09:15 UTC |
| 6c5c3b6 | Andrej Dudenhefner | 07 November 2022, 13:07:48 UTC | replaced complexity by computability | 09 November 2022, 13:32:08 UTC |
| 77653fa | Andrej Dudenhefner | 03 November 2022, 12:56:42 UTC | removed superfluous List, Fin, Vector infrastructure | 09 November 2022, 13:32:07 UTC |
| cd03959 | Andrej Dudenhefner | 02 November 2022, 10:01:15 UTC | typo | 09 November 2022, 13:32:06 UTC |
| 1478286 | Andrej Dudenhefner | 24 October 2022, 15:23:43 UTC | fixed CI | 09 November 2022, 13:32:05 UTC |
| 8b3f76d | Andrej Dudenhefner | 21 October 2022, 15:35:46 UTC | removed smpl dependency | 09 November 2022, 13:31:21 UTC |
| 36f5898 | Andrej Dudenhefner | 21 October 2022, 13:15:51 UTC | removed redundant, complex L_computable_to_TM_computable proof | 09 November 2022, 13:31:20 UTC |
| 80c29a4 | Andrej Dudenhefner | 28 September 2022, 10:49:48 UTC | shown L_computable -> MMA_computable, MMA_computable -> TM_computable added small abstract machine for L (wCBV.v) | 09 November 2022, 13:31:19 UTC |
| 274e2bc | Yannick Forster | 09 November 2022, 13:11:34 UTC | Update README.md | 09 November 2022, 13:11:34 UTC |
| 98d0b21 | DmxLarchey | 09 November 2022, 11:35:22 UTC | cleanup the eq_dec proof with better automation | 09 November 2022, 11:35:22 UTC |
| b591508 | DmxLarchey | 09 November 2022, 10:47:25 UTC | Merge branch 'coq-8.16' into murec_eq_dec | 09 November 2022, 10:47:25 UTC |
| 201b494 | Yannick Forster | 09 November 2022, 09:33:56 UTC | CI for Coq 8.16 (#171) | 09 November 2022, 09:33:56 UTC |
| 4fffe95 | DmxLarchey | 08 November 2022, 20:42:53 UTC | proof of decidable equality for Mu-recursive algorithms based on a component-wise decision for vector equality | 08 November 2022, 20:42:53 UTC |
| c0cbe00 | dominik-kirst | 08 November 2022, 14:54:18 UTC | tricked extensional models | 08 November 2022, 14:54:18 UTC |
| 6b4c39f | Johannes Hostert | 08 November 2022, 02:38:06 UTC | Peano_alt work | 08 November 2022, 02:38:06 UTC |
| 53a25b1 | Johannes Hostert | 02 November 2022, 14:01:47 UTC | Fix bounds solving | 02 November 2022, 14:01:47 UTC |
| c62c79f | Lereau | 03 October 2022, 09:04:26 UTC | fix | 02 November 2022, 13:32:36 UTC |
| db03f09 | Lereau | 02 October 2022, 15:31:21 UTC | fix | 02 November 2022, 13:32:36 UTC |
| 06f1f08 | Lereau | 29 September 2022, 15:54:06 UTC | update | 02 November 2022, 13:32:35 UTC |
| 0c4f41a | Lereau | 29 September 2022, 13:15:54 UTC | update | 02 November 2022, 13:32:33 UTC |
| 7896167 | Lereau | 12 September 2022, 09:57:23 UTC | update | 02 November 2022, 13:30:12 UTC |
| 043b679 | Lereau | 26 July 2022, 07:18:51 UTC | blue | 02 November 2022, 13:22:52 UTC |
| 29ba68f | Lereau | 25 July 2022, 20:35:36 UTC | blue | 02 November 2022, 13:22:39 UTC |
| 5a0f21e | Lereau | 24 July 2022, 18:49:05 UTC | only Euclid missing | 02 November 2022, 13:19:30 UTC |
| 506a385 | Lereau | 24 July 2022, 13:58:35 UTC | Ltac Fold | 02 November 2022, 13:19:28 UTC |
| 45e2257 | Lereau | 23 July 2022, 22:16:37 UTC | equality | 02 November 2022, 13:19:22 UTC |
| 2eeb588 | Andrej Dudenhefner | 02 November 2022, 09:44:21 UTC | Merge pull request #178 from haansn08/to_list_length replace to_list_length with stdlib version | 02 November 2022, 09:44:21 UTC |
| 5fedc20 | Stefan Haan | 30 October 2022, 05:18:41 UTC | replace to_list_length with stdlib version | 30 October 2022, 05:18:41 UTC |
| 573a348 | Andrej Dudenhefner | 21 October 2022, 12:34:43 UTC | Merge pull request #169 from mrhaandi/less-CM2 No CM2 | 21 October 2022, 12:34:43 UTC |
| 21a9451 | Andrej Dudenhefner | 21 October 2022, 08:54:32 UTC | added comment on MPM2 removed several iter_plus definitions | 21 October 2022, 09:02:59 UTC |
| 3035272 | Andrej Dudenhefner | 17 October 2022, 18:16:05 UTC | added comment on Acc and strong normalization | 17 October 2022, 18:24:02 UTC |
| a42761e | Andrej Dudenhefner | 17 October 2022, 18:03:55 UTC | comment on SR2ab | 17 October 2022, 18:24:02 UTC |
| b3073e0 | Andrej Dudenhefner | 19 August 2022, 07:56:27 UTC | replaced CM2 by MM2 in reversible halting, uniform boundedness, and uniform mortality added MM2_dec | 17 October 2022, 18:24:01 UTC |
| bb2c132 | Andrej Dudenhefner | 16 August 2022, 15:22:24 UTC | replaced CM2 by MM2 machine model for CM1_HALT, SSTS01 reduction added MM2_ZERO_HALTING | 17 October 2022, 18:24:00 UTC |
| 224c65c | Andrej Dudenhefner | 17 October 2022, 07:00:09 UTC | Merge pull request #174 from haansn08/patch-1 Update README.md | 17 October 2022, 07:00:09 UTC |
| 3055c01 | haansn08 | 13 October 2022, 14:04:25 UTC | fixed MetaCoq link | 15 October 2022, 15:30:47 UTC |
| b4c75f7 | Andrej Dudenhefner | 14 October 2022, 13:11:19 UTC | Merge pull request #173 from haansn08/prodLists replace prodLists with list_prod from stdlib | 14 October 2022, 13:11:19 UTC |
| c615010 | Stefan Haan | 13 October 2022, 10:43:53 UTC | remove unused lemma prod_nil | 13 October 2022, 10:43:53 UTC |
| 8172c2a | Stefan Haan | 12 October 2022, 13:58:34 UTC | replace prodLists with list_prod from stdlib | 12 October 2022, 13:58:34 UTC |
| 82b92ce | Johannes Hostert | 11 October 2022, 14:05:39 UTC | Fix name confusion | 11 October 2022, 14:05:39 UTC |
| 73c8937 | Johannes Hostert | 11 October 2022, 13:15:31 UTC | Kripke completeness | 11 October 2022, 13:15:31 UTC |
| 3eaa7ee | Andrej Dudenhefner | 10 October 2022, 07:55:24 UTC | Merge pull request #165 from mrhaandi/UTM replaced TM/Univ by top-level UTM construction | 10 October 2022, 07:55:24 UTC |
| c0a4ea3 | Johannes Hostert | 05 October 2022, 21:29:37 UTC | Full Fragment | 05 October 2022, 21:29:37 UTC |
| 548eea0 | Johannes Hostert | 05 October 2022, 20:56:35 UTC | Rework solve_bounds, FSATdc undecidability | 05 October 2022, 20:56:35 UTC |
| 3dbf552 | Johannes Hostert | 05 October 2022, 17:17:27 UTC | Remove redundant enough | 05 October 2022, 17:17:27 UTC |
| 3fc62ea | Johannes Hostert | 05 October 2022, 17:12:12 UTC | MP equivalence | 05 October 2022, 17:12:12 UTC |
| ddb464c | Johannes Hostert | 04 October 2022, 22:29:25 UTC | LEM equivalence analysis | 04 October 2022, 22:29:25 UTC |
| 317af79 | Johannes Hostert | 04 October 2022, 13:57:04 UTC | fragment undec | 04 October 2022, 13:57:04 UTC |
| b4ca16a | dominik-kirst | 04 October 2022, 13:20:18 UTC | cleanup | 04 October 2022, 13:20:18 UTC |
| c35f49b | Johannes Hostert | 04 October 2022, 13:09:27 UTC | Add missing stuff | 04 October 2022, 13:09:27 UTC |
| e5728ad | Johannes Hostert | 04 October 2022, 12:37:20 UTC | More completeness | 04 October 2022, 12:37:56 UTC |
| f564ac5 | dominik-kirst | 04 October 2022, 12:09:59 UTC | general_post_dec | 04 October 2022, 12:09:59 UTC |
| 56f22d4 | Johannes Hostert | 04 October 2022, 00:41:09 UTC | Theorem 4.6 - 4.9 | 04 October 2022, 00:41:09 UTC |
| ef82223 | Johannes Hostert | 03 October 2022, 23:29:36 UTC | SAT undec | 03 October 2022, 23:29:36 UTC |
| bf4c276 | dominik-kirst | 02 October 2022, 13:17:09 UTC | Restructure FSAT, add some missing proofs | 03 October 2022, 22:43:41 UTC |
| e090c5c | dominik-kirst | 02 October 2022, 13:17:09 UTC | PA enum, ksoundness theo, DNE unprovable | 02 October 2022, 13:17:09 UTC |
| 24c041c | dominik-kirst | 01 October 2022, 10:31:16 UTC | prelim facts | 01 October 2022, 10:31:16 UTC |
| 2a0dcd8 | dominik-kirst | 27 September 2022, 10:27:29 UTC | fixed coqdocjs | 27 September 2022, 10:27:29 UTC |
| 535bcb5 | dominik-kirst | 26 September 2022, 12:56:00 UTC | undec of classical minimal logic | 26 September 2022, 12:56:00 UTC |
| 83d2487 | Andrej Dudenhefner | 01 September 2022, 13:05:26 UTC | replaced TM/Univ by top-level UTM construction (Universal, binary Turing machine with 1 tape) | 26 September 2022, 09:05:58 UTC |
| 7d40680 | Andrej Dudenhefner | 26 September 2022, 08:51:02 UTC | Merge pull request #172 from mrhaandi/less-shared replaced parts of Shared/Libs/PSL by stdlib | 26 September 2022, 08:51:02 UTC |
| 9ac039a | Andrej Dudenhefner | 26 September 2022, 08:04:24 UTC | update to latest metacoq | 26 September 2022, 08:34:33 UTC |
