| a95accd | Andrej Dudenhefner | 15 July 2024, 12:46:19 UTC | Merge pull request #220 from mrhaandi/HO-matching Higher-order beta-matching | 15 July 2024, 12:46:19 UTC |
| a1cf0f9 | Andrej Dudenhefner | 17 June 2024, 16:16:12 UTC | Merge pull request #224 from herbelin/master+adapt-coq-pr18591-simpl-never-refolding Adapt to Coq PR #18591: better refolding of List.app inducing "simpl never" now better respected | 17 June 2024, 16:16:12 UTC |
| 0fd2a88 | Hugo Herbelin | 16 June 2024, 12:43:48 UTC | Adapt to Coq PR #18591 which grants "simpl never" on List.app more accuratedly. The change is however indirect: - Coq PR #18591 fixes a lack of refolding of fixpoints; - as a consequence, some calls to "simpl" on subterms start to respect "simpl never" as required; - this impacts "injection" (here the "[]" intro-pattern) as "injection" calls "simpl" on the subterms it generates. | 17 June 2024, 10:12:44 UTC |
| 40d38b1 | Andrej Dudenhefner | 14 June 2024, 08:14:45 UTC | Merge pull request #223 from rlepigre/br/prim-string Adapt to coq/coq#18973. | 14 June 2024, 08:14:45 UTC |
| 789a0ab | Rodolphe Lepigre | 08 June 2024, 12:12:24 UTC | Adapt to coq/coq#18973. | 08 June 2024, 12:12:24 UTC |
| 46d8878 | Andrej Dudenhefner | 10 May 2024, 13:43:54 UTC | Merge pull request #221 from mrhaandi/faster-StepTM improve performance of TM/Single/StepTM.v | 10 May 2024, 13:43:54 UTC |
| ddbb9ba | Andrej Dudenhefner | 10 May 2024, 13:29:56 UTC | improve performance of TM/Single/StepTM.v | 10 May 2024, 13:29:56 UTC |
| 1eb2a05 | Andrej Dudenhefner | 22 April 2024, 13:37:33 UTC | added HOMbeta (higher-order matching wrt. beta-equivalence) added reduction from SSTS01 to HOMbeta | 22 April 2024, 13:48:35 UTC |
| a32c928 | Andrej Dudenhefner | 04 April 2024, 10:17:05 UTC | Merge pull request #219 from mrhaandi/address-8-20-warnings Address Coq 8.20 warnings | 04 April 2024, 10:17:05 UTC |
| f9e11e1 | Andrej Dudenhefner | 04 April 2024, 09:33:42 UTC | addressed Coq 8.20 warnings | 04 April 2024, 09:59:35 UTC |
| f6e126c | Andrej Dudenhefner | 30 January 2024, 08:41:20 UTC | Merge pull request #217 from andres-erbsen/coq-more-nth_error Adapt for coq/coq#18563 | 30 January 2024, 08:41:20 UTC |
| 8a904da | Andres Erbsen | 29 January 2024, 17:02:44 UTC | adapt for coq/coq#18563 | 29 January 2024, 17:02:44 UTC |
| 47b4b27 | Gaëtan Gilbert | 29 January 2024, 13:26:26 UTC | Adapt to metacoq primitive arrays | 29 January 2024, 13:29:34 UTC |
| 91165e2 | Andrej Dudenhefner | 03 November 2023, 11:26:52 UTC | Merge pull request #215 from proux01/coq_17576 Adapt to https://github.com/coq/coq/pull/17576 | 03 November 2023, 11:26:52 UTC |
| af4711d | Pierre Roux | 03 November 2023, 09:30:10 UTC | Adapt to https://github.com/coq/coq/pull/17576 | 03 November 2023, 09:33:43 UTC |
| cc216ff | Andrej Dudenhefner | 19 October 2023, 14:34:53 UTC | Merge pull request #210 from mrhaandi/rm_arith_files adapt to https://github.com/coq/coq/pull/18164 | 19 October 2023, 14:34:53 UTC |
| 5376bd8 | Andrej Dudenhefner | 19 October 2023, 14:15:42 UTC | adapt to https://github.com/coq/coq/pull/18164 | 19 October 2023, 14:15:42 UTC |
| bddbe03 | Dominique Larchey-Wendling | 09 October 2023, 13:23:33 UTC | As agreed, remove the reference to the former CeCILL v2 license (second step) (#209) * relicense to MPL-2.0 using a script * changing license field in opam file, thx to @Zimmi48 * renamed MPL-2.0 license file for GitHub automatic recognition * removed reference to former CeCILL license | 09 October 2023, 13:23:33 UTC |
| 52882f2 | Dominique Larchey-Wendling | 09 October 2023, 08:41:44 UTC | Change license from CeCILL v2 to MPL-2.0 (more permissive) (#208) * relicense to MPL-2.0 using a script * changing license field in opam file, thx to @Zimmi48 * renamed MPL-2.0 license file for GitHub automatic recognition | 09 October 2023, 08:41:44 UTC |
| fea1078 | Andrej Dudenhefner | 30 August 2023, 08:55:41 UTC | Merge pull request #206 from mrhaandi/fix-coq-17129 Fix coq-17129 | 30 August 2023, 08:55:41 UTC |
| 882d2a7 | Andrej Dudenhefner | 30 August 2023, 08:36:51 UTC | fix dependency for https://github.com/coq/coq/pull/17129 | 30 August 2023, 08:36:51 UTC |
| a7f4b4f | Andrej Dudenhefner | 24 August 2023, 16:45:23 UTC | Merge pull request #205 from mrhaandi/lambda-cap-full Add Intersection Type related problems | 24 August 2023, 16:45:23 UTC |
| 1520ce9 | Andrej Dudenhefner | 24 August 2023, 07:39:32 UTC | changed "the lambda-calculus" to "strong call-by-name lambda-calculus" changed (scons t var) to (scons t (fun x => var x)) | 24 August 2023, 14:43:24 UTC |
| 66766f6 | Andrej Dudenhefner | 23 August 2023, 12:49:20 UTC | added problems intersection type inhabitation, typability, type checking added reduction from intersection type typability to intersection type type checking added reduction from strong normalization to intersection type typability added reduction from simple semi-Thue system 01 rewriting to intersection type inhabitation | 23 August 2023, 12:49:20 UTC |
| 10d19ec | Andrej Dudenhefner | 23 August 2023, 12:41:14 UTC | added problem strong normalization wrt. beta-reduction in the lambda-calculus added reduction from Krivine machine halting to strong normalization | 23 August 2023, 12:41:14 UTC |
| 0095944 | Andrej Dudenhefner | 31 July 2023, 12:51:21 UTC | Merge pull request #204 from mrhaandi/faster-KOSBTM faster HaltKOSBTM_to_HaltBSM.v | 31 July 2023, 12:51:21 UTC |
| fb0d50b | Andrej Dudenhefner | 31 July 2023, 09:31:59 UTC | faster HaltKOSBTM_to_HaltBSM.v | 31 July 2023, 11:21:12 UTC |
| 0295fb8 | Andrej Dudenhefner | 27 July 2023, 14:31:07 UTC | Merge pull request #203 from mrhaandi/refactor-L_computable_closed Refactor L_computable_closed | 27 July 2023, 14:31:07 UTC |
| f7be455 | Andrej Dudenhefner | 26 July 2023, 14:03:52 UTC | more concise L/Datatypes/Lists | 27 July 2023, 13:57:41 UTC |
| 637dab8 | Andrej Dudenhefner | 26 July 2023, 13:43:36 UTC | refactor L_computable and L_computable_closed to improve most time consuming compilation path | 26 July 2023, 13:43:36 UTC |
| 4764e06 | Andrej Dudenhefner | 12 July 2023, 13:27:36 UTC | Merge pull request #202 from mrhaandi/coq-8.18-nowarn No warnings for Coq 8.18 | 12 July 2023, 13:27:36 UTC |
| d51fae6 | Andrej Dudenhefner | 12 July 2023, 10:03:53 UTC | no warnings for Coq 8.18 muted 500 Let...Qed warnings | 12 July 2023, 12:22:14 UTC |
| 0e29426 | Yannick Forster | 05 May 2023, 11:19:51 UTC | Merge pull request #199 from ppedrot/case-pf-pose-dependent-metas Adapt w.r.t. coq/coq#17564. | 05 May 2023, 11:19:51 UTC |
| a6920b9 | Pierre-Marie Pédrot | 05 May 2023, 08:20:23 UTC | Adapt w.r.t. coq/coq#17564. | 05 May 2023, 08:20:23 UTC |
| b2fdda7 | Andrej Dudenhefner | 27 April 2023, 11:16:47 UTC | Merge pull request #198 from mrhaandi/fix-coq-17538 follow up on fix for coq 17538 | 27 April 2023, 11:16:47 UTC |
| 811b7f1 | Andrej Dudenhefner | 27 April 2023, 11:15:41 UTC | follow up on https://github.com/coq/coq/pull/17538 fix | 27 April 2023, 11:15:41 UTC |
| e36cfb2 | Yannick Forster | 27 April 2023, 09:14:18 UTC | Merge pull request #196 from mrhaandi/fix-coq-17538 | 27 April 2023, 09:14:18 UTC |
| b84bd34 | Andrej Dudenhefner | 27 April 2023, 08:16:37 UTC | fix for https://github.com/coq/coq/pull/17538 update README.md | 27 April 2023, 08:16:37 UTC |
| c1110b0 | Andrej Dudenhefner | 11 April 2023, 11:27:04 UTC | Merge pull request #194 from mrhaandi/fasterZF Faster ZF | 11 April 2023, 11:27:04 UTC |
| 62975f9 | Andrej Dudenhefner | 11 April 2023, 10:52:48 UTC | faster PCPb_to_binZF.v and PCPb_to_minZF.v | 11 April 2023, 11:01:57 UTC |
| 2938761 | Yannick Forster | 06 April 2023, 11:21:30 UTC | fix CI | 06 April 2023, 11:21:30 UTC |
| 1f48c81 | Andrej Dudenhefner | 05 April 2023, 10:01:51 UTC | preparations/simplifications for Coq 8.17 | 05 April 2023, 13:13:57 UTC |
| cfa228f | Andrej Dudenhefner | 28 February 2023, 08:38:08 UTC | Merge pull request #191 from LasseBlaauwbroek/overlay-17304 Adapt w.r.t. coq/coq#17304 | 28 February 2023, 08:38:08 UTC |
| bc307de | Lasse Blaauwbroek | 28 February 2023, 02:14:58 UTC | Adapt w.r.t. coq/coq#17304 Should be backwards compatible. | 28 February 2023, 02:14:58 UTC |
| ad2c788 | Yannick Forster | 09 February 2023, 10:14:06 UTC | add CI for master | 09 February 2023, 10:14:06 UTC |
| 4547d32 | Andrej Dudenhefner | 08 February 2023, 12:39:18 UTC | added tentative instructions | 08 February 2023, 12:39:18 UTC |
| b07efe7 | Andrej Dudenhefner | 08 February 2023, 09:47:24 UTC | compatibility with Coq 8.17 (no warnings/errors) | 08 February 2023, 10:48:42 UTC |
| 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 |
