| 4115398 | Dominique Larchey-Wendling | 01 May 2021, 09:38:37 UTC | insist of coq-8.13 | 01 May 2021, 09:38:37 UTC |
| 0235107 | Dominique Larchey-Wendling | 01 May 2021, 09:36:16 UTC | added mandatory for coq 8.13 | 01 May 2021, 09:36:16 UTC |
| 1d5bf3b | Dominique Larchey-Wendling | 01 May 2021, 09:30:06 UTC | better sentence | 01 May 2021, 09:30:06 UTC |
| 881396d | Dominique Larchey-Wendling | 01 May 2021, 09:29:20 UTC | date of the forking/freezing from coq-8.13 | 01 May 2021, 09:29:20 UTC |
| 03fa4df | Dominique Larchey-Wendling | 01 May 2021, 09:25:59 UTC | further comment about dependencies | 01 May 2021, 09:25:59 UTC |
| 74342da | Dominique Larchey-Wendling | 01 May 2021, 09:23:50 UTC | uodate readme file | 01 May 2021, 09:23:50 UTC |
| a039006 | Dominique Larchey-Wendling | 01 May 2021, 09:21:08 UTC | try another link to archived ZIP | 01 May 2021, 09:21:08 UTC |
| 3a2f4fb | Dominique Larchey-Wendling | 01 May 2021, 09:17:54 UTC | This branch will disappear once the tag on created | 01 May 2021, 09:17:54 UTC |
| 8d348a4 | Dominique Larchey-Wendling | 01 May 2021, 09:14:26 UTC | update the README for coq-8.13 | 01 May 2021, 09:14:26 UTC |
| c5fbf8f | Dominique Larchey-Wendling | 01 May 2021, 09:06:32 UTC | Specialized Readme.v file for the FSCD-2021 paper | 01 May 2021, 09:06:32 UTC |
| c6d1e81 | Dominique Larchey-Wendling | 23 April 2021, 16:32:52 UTC | Merge pull request #126 from DmxLarchey/imsell-8.13 Improvements (notations, shorter proofs, etc) for IMSELL | 23 April 2021, 16:32:52 UTC |
| 87c8e77 | Dominique Larchey-Wendling | 23 April 2021, 14:13:31 UTC | Merge branch 'coq-8.13' into imsell-8.13 | 23 April 2021, 14:13:31 UTC |
| 8e50d80 | Dominique Larchey-Wendling | 23 April 2021, 14:01:30 UTC | forgot to commit that correction | 23 April 2021, 14:01:30 UTC |
| 95f9062 | Yannick Forster | 23 April 2021, 13:17:47 UTC | Merge pull request #125 from yforster/coq-8.13-update-README Update README in 8.13 branch | 23 April 2021, 13:17:47 UTC |
| d59f976 | Dominique Larchey-Wendling | 23 April 2021, 12:20:57 UTC | Merge branch 'coq-8.13' into imsell-8.13 | 23 April 2021, 12:20:57 UTC |
| e4d2b50 | Yannick Forster | 23 April 2021, 08:47:57 UTC | Update README | 23 April 2021, 08:47:57 UTC |
| f88f319 | Dominique Larchey-Wendling | 21 April 2021, 09:36:50 UTC | Merge branch 'coq-8.12' into imsell | 21 April 2021, 09:36:50 UTC |
| b5f6b87 | Yannick Forster | 14 April 2021, 08:23:09 UTC | Merge pull request #121 from uds-psl/yforster-patch-1 Add mu recursive functions to README | 14 April 2021, 08:23:09 UTC |
| 38d97c5 | Yannick Forster | 12 April 2021, 09:21:53 UTC | Add mu recursive functions to README | 12 April 2021, 09:21:53 UTC |
| 54550f6 | Yannick Forster | 29 March 2021, 11:53:46 UTC | Merge pull request #116 from dominik-kirst/seplogic Separation Logic | 29 March 2021, 11:53:46 UTC |
| 0f3fd61 | Dominik Kirst | 19 March 2021, 12:48:02 UTC | improved readme and changed file and problem names | 19 March 2021, 12:48:02 UTC |
| 1ed38fe | Dominik Kirst | 19 March 2021, 12:25:52 UTC | quantifier notations in comments | 19 March 2021, 12:25:52 UTC |
| bde7a60 | Dominik Kirst | 19 March 2021, 12:21:23 UTC | Merge pull request #1 from DmxLarchey/seplogic-dlw A module for FOL notations within TRAHKTENBROT | 19 March 2021, 12:21:23 UTC |
| 9db05e0 | Dominique Larchey-Wendling | 19 March 2021, 12:01:41 UTC | A module for fol_notations | 19 March 2021, 12:01:41 UTC |
| 91bd889 | Dominik Kirst | 18 March 2021, 16:30:16 UTC | proof using flag | 18 March 2021, 16:30:16 UTC |
| 6bf9427 | Dominik Kirst | 18 March 2021, 16:16:43 UTC | readme | 18 March 2021, 16:16:43 UTC |
| 9d81434 | Dominik Kirst | 18 March 2021, 14:23:56 UTC | cleanup | 18 March 2021, 14:23:56 UTC |
| 09388f0 | Dominik Kirst | 17 March 2021, 17:17:28 UTC | undec files | 17 March 2021, 17:17:28 UTC |
| b5d9983 | Dominik Kirst | 17 March 2021, 11:34:48 UTC | reduction from trakhtenbrot to new fsat | 17 March 2021, 11:34:48 UTC |
| a000c6c | Dominik Kirst | 17 March 2021, 10:30:00 UTC | switched quantifier notation | 17 March 2021, 10:30:00 UTC |
| 41bf7a2 | Dominik Kirst | 16 March 2021, 17:26:24 UTC | reduction for closed FSAT | 16 March 2021, 17:26:24 UTC |
| 0bb50d8 | Dominik Kirst | 15 March 2021, 13:21:49 UTC | finished rest of requirements | 15 March 2021, 13:21:49 UTC |
| e23c755 | Dominik Kirst | 15 March 2021, 12:45:13 UTC | half of missing requirements | 15 March 2021, 12:45:13 UTC |
| 0a2e328 | Dominik Kirst | 12 March 2021, 17:27:48 UTC | done up to model requirements | 12 March 2021, 17:27:48 UTC |
| b32e2a1 | Dominik Kirst | 12 March 2021, 16:39:31 UTC | finished up to requirements and final proof | 12 March 2021, 16:39:31 UTC |
| a5b5683 | Dominik Kirst | 12 March 2021, 16:17:57 UTC | closed main proofs | 12 March 2021, 16:17:57 UTC |
| bb831c2 | Dominik Kirst | 12 March 2021, 14:21:38 UTC | improvements | 12 March 2021, 14:21:38 UTC |
| 24712de | Dominik Kirst | 12 March 2021, 11:38:53 UTC | backwards direction | 12 March 2021, 11:38:53 UTC |
| 6dd38f5 | Dominik Kirst | 11 March 2021, 17:34:08 UTC | encoding function from FOL FSAT to min_seplogic | 11 March 2021, 17:34:08 UTC |
| 46d0fb2 | Dominik Kirst | 11 March 2021, 12:17:00 UTC | switched to de bruijn syntax | 11 March 2021, 12:17:00 UTC |
| 705dd73 | Dominik Kirst | 10 March 2021, 18:29:44 UTC | functionality constraint | 10 March 2021, 18:29:44 UTC |
| 368e469 | Dominik Kirst | 10 March 2021, 16:17:04 UTC | epsilon | 10 March 2021, 16:17:04 UTC |
| b796dc9 | Dominik Kirst | 10 March 2021, 16:15:57 UTC | example and little fix | 10 March 2021, 16:15:57 UTC |
| fad7b10 | Dominik Kirst | 10 March 2021, 15:19:55 UTC | two fragments of separation logic | 10 March 2021, 15:19:55 UTC |
| 77276a0 | Yannick Forster | 10 March 2021, 09:29:45 UTC | Merge pull request #113 from yforster/neq_coq-8.13 Merge 8.12 into 8.13 to prepare for opam release | 10 March 2021, 09:29:45 UTC |
| a9d60ea | Yannick Forster | 02 March 2021, 14:23:54 UTC | Use MetaCoq 1.0~beta2 on coq-8.12 (#114) * use MetaCoq 1.0~beta2, getting rid of the checker dependency * fix Extract.v * fix GenEncode.v * remove broken and unused Notation * fix rewrites | 02 March 2021, 14:23:54 UTC |
| cfcd4c7 | Yannick Forster | 02 March 2021, 14:22:59 UTC | Merge pull request #1 from mrhaandi/neq_coq-8.13 fixed warnings | 02 March 2021, 14:22:59 UTC |
| 4690ec2 | Andrej Dudenhefner | 02 March 2021, 13:01:02 UTC | fixed warnings set coq to 8.13.1 | 02 March 2021, 13:01:02 UTC |
| 100c9a1 | Dominique Larchey-Wendling | 26 February 2021, 14:02:51 UTC | divides_dec in fractran_step_dec | 26 February 2021, 14:02:51 UTC |
| 30e0c1a | Yannick Forster | 24 February 2021, 08:40:39 UTC | fix setoid rewriting bug | 24 February 2021, 08:40:39 UTC |
| 5a651b9 | Dominique Larchey-Wendling | 23 February 2021, 22:38:25 UTC | change the reduction chain FRACTRAN <= MMA2 <= MM2 <= ndMM2 to FRACTRAN <= MMA2 <= ndMM2 | 23 February 2021, 22:38:25 UTC |
| 7883c17 | Yannick Forster | 23 February 2021, 09:58:04 UTC | fix FOL under 8.13 | 23 February 2021, 09:58:04 UTC |
| fb04c32 | Yannick Forster | 23 February 2021, 09:01:12 UTC | fix typo in MetaCoq version | 23 February 2021, 09:01:12 UTC |
| 1f3e551 | Yannick Forster | 23 February 2021, 08:00:16 UTC | restart CI | 23 February 2021, 08:00:16 UTC |
| 97d5db4 | Dominique Larchey-Wendling | 22 February 2021, 22:55:21 UTC | more generic def of MMA_PROBLEM | 22 February 2021, 22:55:21 UTC |
| 6347f0d | Yannick Forster | 22 February 2021, 16:15:44 UTC | fix equations version | 22 February 2021, 16:15:44 UTC |
| fb0c262 | Yannick Forster | 22 February 2021, 16:00:57 UTC | use released MetaCoq packages | 22 February 2021, 16:00:57 UTC |
| b6d68dd | Yannick Forster | 22 February 2021, 15:56:54 UTC | Merge branch 'coq-8.12' into neq_coq-8.13 | 22 February 2021, 15:56:54 UTC |
| 8e170e6 | Dominique Larchey-Wendling | 22 February 2021, 08:53:32 UTC | slight ups | 22 February 2021, 08:53:32 UTC |
| 8afdc22 | Dominique Larchey-Wendling | 15 February 2021, 14:51:53 UTC | small ups in notations mostly | 15 February 2021, 14:51:53 UTC |
| 9396e87 | Dominique Larchey-Wendling | 08 February 2021, 15:04:46 UTC | loops no needed anymore | 08 February 2021, 15:04:46 UTC |
| 19822b1 | Dominique Larchey-Wendling | 06 February 2021, 23:28:08 UTC | forgot to update some code for the small changes | 06 February 2021, 23:28:08 UTC |
| 97e9e19 | Dominique Larchey-Wendling | 06 February 2021, 23:18:57 UTC | removed the need of super-regularity ... the reduction already worked for regular Fractran programs | 06 February 2021, 23:18:57 UTC |
| 6830557 | Dominique Larchey-Wendling | 06 February 2021, 23:00:31 UTC | Notations mostly | 06 February 2021, 23:00:31 UTC |
| c6b3cd0 | Dominique Larchey-Wendling | 02 February 2021, 23:45:41 UTC | change in notation for shorter notations | 02 February 2021, 23:45:41 UTC |
| 8b870ad | Dominique Larchey-Wendling | 02 February 2021, 13:52:22 UTC | Merge remote-tracking branch 'upstream/coq-8.12' into mma_ndmm | 02 February 2021, 13:52:22 UTC |
| 24aec42 | Dominique Larchey-Wendling | 02 February 2021, 13:39:29 UTC | changed "by lia" into "unfold z2; lia" in SMN_transform.v Do not know why "by lia" failed in Coq 8.12.0 ? | 02 February 2021, 13:39:29 UTC |
| 37f3507 | Dominique Larchey-Wendling | 02 February 2021, 13:20:38 UTC | a shared reduction from FRACTRAN_REG_HALING to both MMA2_HALTING and MMA2_HALTS_ON_ZERO. This avoids the detour through the compiler for the reduction from MMA2_HALTING to MMA2_HALTS_ON_ZERO, hence avoids having to describe it in a paper | 02 February 2021, 13:20:38 UTC |
| bcdf0e8 | Yannick Forster | 30 January 2021, 12:53:43 UTC | Merge pull request #111 from dominik-kirst/itp Peano Arithmetic, Binary ZF, Binary FOL | 30 January 2021, 12:53:43 UTC |
| c7c88f4 | Dominik Kirst | 30 January 2021, 11:44:29 UTC | readme, using vector notations, moved syntax fragments | 30 January 2021, 11:44:29 UTC |
| 17193a5 | Dominik Kirst | 29 January 2021, 21:56:48 UTC | incompleteness proof up to enumerability | 29 January 2021, 21:56:48 UTC |
| eb1d468 | Marc Hermes | 29 January 2021, 20:24:40 UTC | changes in Axiomatisations | 29 January 2021, 20:24:40 UTC |
| 53795e0 | Dominik Kirst | 27 January 2021, 18:02:21 UTC | refactored H10p reduction | 27 January 2021, 18:02:21 UTC |
| 4c08471 | Marc Hermes | 26 January 2021, 16:51:23 UTC | Merge branch 'itp' of https://github.com/dominik-kirst/coq-library-undecidability into itp | 26 January 2021, 16:51:23 UTC |
| b197e1b | Marc Hermes | 26 January 2021, 16:51:15 UTC | added Axiomatisations.v | 26 January 2021, 16:51:15 UTC |
| 0ed4b81 | Dominik Kirst | 26 January 2021, 12:42:39 UTC | reductions without assumptions | 26 January 2021, 12:42:39 UTC |
| c4b8861 | Dominik Kirst | 26 January 2021, 11:19:00 UTC | undec of binary FOL | 26 January 2021, 11:19:00 UTC |
| e3eafec | Dominik Kirst | 26 January 2021, 10:26:13 UTC | Merge branch 'itp' of https://github.com/dominik-kirst/coq-library-undecidability into itp | 26 January 2021, 10:26:13 UTC |
| 0f0b55b | Dominik Kirst | 26 January 2021, 10:26:08 UTC | closed binZF proof | 26 January 2021, 10:26:08 UTC |
| a9e1a2f | Marc Hermes | 26 January 2021, 10:23:02 UTC | clear up in PA reduction | 26 January 2021, 10:23:02 UTC |
| 20a6c41 | Dominik Kirst | 26 January 2021, 10:14:23 UTC | one admit left | 26 January 2021, 10:14:23 UTC |
| cb90f97 | Dominik Kirst | 26 January 2021, 09:25:02 UTC | only morphism lemmas left | 26 January 2021, 09:25:02 UTC |
| c699f72 | Dominik Kirst | 26 January 2021, 08:56:04 UTC | proved first admit | 26 January 2021, 08:56:04 UTC |
| 0c3ed9f | Dominik Kirst | 25 January 2021, 20:20:46 UTC | Merge branch 'itp' of https://github.com/dominik-kirst/coq-library-undecidability into itp | 25 January 2021, 20:20:46 UTC |
| 7ee0371 | Dominik Kirst | 25 January 2021, 20:20:37 UTC | intensional verification to get rid of CE | 25 January 2021, 20:20:37 UTC |
| 140249f | Marc Hermes | 25 January 2021, 20:14:49 UTC | quick fix | 25 January 2021, 20:14:49 UTC |
| 5ca71b2 | Marc Hermes | 25 January 2021, 20:08:07 UTC | Version 2 done. Semantic part completed | 25 January 2021, 20:08:07 UTC |
| 4258f7e | Marc Hermes | 25 January 2021, 18:58:08 UTC | Merge branch 'itp' of https://github.com/dominik-kirst/coq-library-undecidability into itp | 25 January 2021, 18:58:08 UTC |
| 75f68a2 | Marc Hermes | 25 January 2021, 18:58:02 UTC | Version 1 of H10p to PA is done | 25 January 2021, 18:58:02 UTC |
| 5d5d1b8 | Dominik Kirst | 25 January 2021, 17:30:25 UTC | missing proof for vector lemma | 25 January 2021, 17:30:25 UTC |
| da1b2e1 | Dominik Kirst | 25 January 2021, 17:16:46 UTC | bounds tactic | 25 January 2021, 17:16:46 UTC |
| 7d453a9 | Marc Hermes | 25 January 2021, 16:15:01 UTC | push | 25 January 2021, 16:15:01 UTC |
| c5924bd | Marc Hermes | 25 January 2021, 14:18:38 UTC | quick fix | 25 January 2021, 14:18:38 UTC |
| ef8418b | Marc Hermes | 25 January 2021, 14:08:27 UTC | bounded_ext done | 25 January 2021, 14:08:27 UTC |
| fdaab85 | Marc Hermes | 25 January 2021, 14:06:02 UTC | bounded_ext done | 25 January 2021, 14:06:02 UTC |
| 3bc4a24 | Dominik Kirst | 25 January 2021, 12:40:17 UTC | changed implication notations | 25 January 2021, 12:40:17 UTC |
| 98e1bca | Dominik Kirst | 25 January 2021, 11:31:03 UTC | intensional model | 25 January 2021, 11:31:03 UTC |
| 680e7e7 | Marc Hermes | 24 January 2021, 18:39:29 UTC | added FA Utils | 24 January 2021, 18:39:29 UTC |
| 88e2d16 | Marc Hermes | 24 January 2021, 18:34:48 UTC | small fix | 24 January 2021, 18:34:48 UTC |
| 4271b77 | Dominik Kirst | 24 January 2021, 11:55:31 UTC | lemma structure for first half of translation | 24 January 2021, 11:55:31 UTC |
