| c389de7 | Yannick Forster | 21 April 2020, 15:17:09 UTC | Merge pull request #48 from fakusb/coq-8.11-comp-only Refactored changes from private complexity-development | 21 April 2020, 15:17:09 UTC |
| f4db3ff | Fabian Kunze | 21 April 2020, 12:33:15 UTC | reenabled unused-intro-pattern warnings by default as the TM-framework disables them for all files that import the tactic causing them | 21 April 2020, 12:33:15 UTC |
| 5e60394 | Yannick Forster | 21 April 2020, 10:58:33 UTC | No warnings left | 21 April 2020, 10:58:33 UTC |
| bf41863 | Fabian Kunze | 21 April 2020, 09:24:42 UTC | -removed unneeded files -changed compilation order for better utilization of multi-core compilation (start large, monolithic files early) | 21 April 2020, 09:24:42 UTC |
| bb747c7 | Fabian Kunze | 20 April 2020, 14:58:25 UTC | refactored changes from private complexity-development in TM and L-extraction/verification frameworks | 20 April 2020, 16:42:57 UTC |
| d717806 | Dominique Larchey-Wendling | 20 April 2020, 12:52:43 UTC | Merge pull request #47 from DmxLarchey/unify_Fin_pos Unify Fin.t / pos and Vector.t / vec | 20 April 2020, 12:52:43 UTC |
| 14775e7 | Dominique Larchey-Wendling | 20 April 2020, 10:00:33 UTC | more cleanup in pos/vec | 20 April 2020, 10:00:33 UTC |
| 83ca25b | Dominique Larchey-Wendling | 19 April 2020, 16:08:37 UTC | unified Vector.t and vec ... several problems. 1) vec_cons can no longer be used as a constructor but the notation _ ## _ can largely mitigate 2) Vector.cons X x n v = vec_cons X n x v ie the arguments are no in the same order. Ie when invoquing induction we explicit intro pattern, you need to rearrange arguments 3) default parameter names are diffents, typical v is replaced by t which means scripts that use autogenerated names will likely fail ... | 19 April 2020, 16:08:37 UTC |
| 968ddf4 | Dominique Larchey-Wendling | 19 April 2020, 14:46:48 UTC | Unified Fin.t and pos so that they are now identical instead of just isomorphic | 19 April 2020, 14:46:48 UTC |
| 7ffb6a8 | Yannick Forster | 15 April 2020, 10:37:57 UTC | Merge pull request #43 from yforster/remove_more_warnings Remove more warnings in L and TM | 15 April 2020, 10:37:57 UTC |
| c3931b6 | Dominique Larchey-Wendling | 15 April 2020, 09:36:24 UTC | removed unnecessary Checks in library files | 15 April 2020, 09:36:24 UTC |
| 94522db | Yannick Forster | 15 April 2020, 08:34:35 UTC | Remove last warnings, remove more printing | 15 April 2020, 08:34:35 UTC |
| 67b68e6 | Yannick Forster | 15 April 2020, 07:01:21 UTC | remove more printing | 15 April 2020, 07:01:21 UTC |
| 455aa7a | Dominique Larchey-Wendling | 14 April 2020, 23:50:18 UTC | forgot to update bool_list.v and seqeq.v | 14 April 2020, 23:50:18 UTC |
| 2d1088e | Dominique Larchey-Wendling | 14 April 2020, 21:41:28 UTC | update Shared/Libs/DLW for ": core" hints warnings | 14 April 2020, 21:41:28 UTC |
| 26cb31b | Yannick Forster | 14 April 2020, 17:01:26 UTC | Remove last warnings | 14 April 2020, 17:01:26 UTC |
| 383a144 | Yannick Forster | 14 April 2020, 16:38:37 UTC | Remove lots of warnings in L and TM parts | 14 April 2020, 16:38:37 UTC |
| 3ad4cb8 | Yannick Forster | 14 April 2020, 13:00:29 UTC | fix opam repo add | 14 April 2020, 13:00:33 UTC |
| 64ecf83 | Yannick Forster | 14 April 2020, 08:07:40 UTC | Update License | 14 April 2020, 13:00:33 UTC |
| e7a7d52 | Yannick Forster | 14 April 2020, 08:06:48 UTC | Update README | 14 April 2020, 13:00:33 UTC |
| af4263c | Yannick Forster | 14 April 2020, 12:59:16 UTC | Merge pull request #40 from mrhaandi/coq-8.11-nowarn Less Warnings, Improved Compilation Speed | 14 April 2020, 12:59:16 UTC |
| 44c839e | mrhaandi | 14 April 2020, 11:54:16 UTC | merged TRAKHTENBROT from upstream | 14 April 2020, 11:54:16 UTC |
| bf25a30 | Yannick Forster | 14 April 2020, 10:49:40 UTC | Merge pull request #41 from DmxLarchey/trakhtenbrot Proposal to integrate the Trakhtenbrot code (IJCAR 2020) | 14 April 2020, 10:49:40 UTC |
| 33bb80d | Dominique Larchey-Wendling | 13 April 2020, 17:30:55 UTC | Dispatched Problems/PCP.v into PCP/PCP.c PCP/Reductions/*_iff*.v | 13 April 2020, 17:30:55 UTC |
| bc33a60 | Dominique Larchey-Wendling | 13 April 2020, 09:35:56 UTC | informativelly_reduces | 13 April 2020, 09:35:56 UTC |
| 09c23a9 | Dominique Larchey-Wendling | 11 April 2020, 21:24:44 UTC | Merge pull request #10 from DmxLarchey/ij1 integrated the TRAKHTENBROT code with informative reductions | 11 April 2020, 21:24:44 UTC |
| 131ba49 | Dominique Larchey-Wendling | 11 April 2020, 21:22:23 UTC | integrated the TRAKHTENBROT code with informative reductions | 11 April 2020, 21:22:23 UTC |
| f1bde74 | Dominique Larchey-Wendling | 11 April 2020, 20:46:05 UTC | Merge pull request #9 from DmxLarchey/ij1 merging Problems/*.v and Shared/Prelims.v for the Trakhtenbrot devel | 11 April 2020, 20:46:05 UTC |
| aed0a05 | Dominique Larchey-Wendling | 11 April 2020, 20:44:34 UTC | informative and non-informative reductions | 11 April 2020, 20:44:34 UTC |
| 237ea69 | Dominique Larchey-Wendling | 11 April 2020, 20:18:10 UTC | merging Problems/*.v and Shared/Prelims.v for the Trakhtenbrot devel | 11 April 2020, 20:18:10 UTC |
| 29b03ef | Dominique Larchey-Wendling | 11 April 2020, 20:10:02 UTC | Merge pull request #8 from DmxLarchey/ij1 Merge libs from trakhtenbrot | 11 April 2020, 20:10:02 UTC |
| 13c9b20 | Dominique Larchey-Wendling | 11 April 2020, 20:03:21 UTC | removed one cutrewrite | 11 April 2020, 20:03:21 UTC |
| 3b184e1 | Dominique Larchey-Wendling | 11 April 2020, 19:53:18 UTC | reverted orig libs | 11 April 2020, 19:53:18 UTC |
| 109cbb7 | Dominique Larchey-Wendling | 11 April 2020, 19:44:16 UTC | Revert "Delete vec.v" This reverts commit 1991a25ab6b82f256292db63ce90100454f212c7. | 11 April 2020, 19:44:16 UTC |
| 1991a25 | Dominique Larchey-Wendling | 11 April 2020, 19:38:32 UTC | Delete vec.v | 11 April 2020, 19:38:32 UTC |
| 6cbf46e | Dominique Larchey-Wendling | 11 April 2020, 19:29:10 UTC | to compare with the IJCAR lib | 11 April 2020, 19:29:10 UTC |
| 645aeb1 | Dominique Larchey-Wendling | 11 April 2020, 19:02:34 UTC | removed warnings | 11 April 2020, 19:02:34 UTC |
| ec2650d | Dominique Larchey-Wendling | 11 April 2020, 09:14:19 UTC | Merge pull request #5 from DmxLarchey/libs_update Libs update | 11 April 2020, 09:14:19 UTC |
| a3f8fee | mrhaandi | 10 April 2020, 18:14:31 UTC | replaced cutrewrite (x = y) by replace x with y | 10 April 2020, 18:14:31 UTC |
| f7f3190 | mrhaandi | 10 April 2020, 17:57:08 UTC | removed some minor warnings | 10 April 2020, 17:57:08 UTC |
| e1baf70 | mrhaandi | 10 April 2020, 17:39:31 UTC | small LAM and TM warning fixes | 10 April 2020, 17:39:31 UTC |
| 3b034e5 | mrhaandi | 10 April 2020, 17:05:02 UTC | dealt with warnings in HOU | 10 April 2020, 17:05:02 UTC |
| 365a80b | mrhaandi | 10 April 2020, 16:41:18 UTC | dealt with ILL warnings | 10 April 2020, 16:41:18 UTC |
| edae7bf | mrhaandi | 10 April 2020, 15:24:48 UTC | dealt with warnings in MuRec | 10 April 2020, 15:24:48 UTC |
| 08f37e5 | mrhaandi | 10 April 2020, 14:58:44 UTC | dealt with warnings in H10 | 10 April 2020, 14:58:44 UTC |
| d21270a | mrhaandi | 10 April 2020, 13:30:03 UTC | no warnings in MM | 10 April 2020, 13:30:03 UTC |
| 8fb7469 | mrhaandi | 10 April 2020, 12:29:56 UTC | improved PCP, CFG, SR compilation speed eliminated PCP, CFG, SR compilation warnings removed several Print Assumptions, improving compilation speed | 10 April 2020, 12:29:56 UTC |
| 12848be | Yannick Forster | 09 April 2020, 14:47:13 UTC | Update README.md | 09 April 2020, 14:47:13 UTC |
| 4a55a78 | Yannick Forster | 09 April 2020, 14:35:58 UTC | Update README.md | 09 April 2020, 14:35:58 UTC |
| 009c1ca | Yannick Forster | 06 April 2020, 13:38:25 UTC | Merge pull request #39 from mrhaandi/coq-8.11 PCP refactoring into PCP, SR, GFG | 06 April 2020, 13:38:25 UTC |
| 1ad3985 | mrhaandi | 31 March 2020, 15:29:53 UTC | removed outdated readme | 31 March 2020, 15:29:53 UTC |
| 1c7c739 | mrhaandi | 31 March 2020, 15:15:51 UTC | refactored PCP into PCP, SR, CFG removed Shared.Prelim from Problems.Reduction | 31 March 2020, 15:15:51 UTC |
| 825008f | Yannick Forster | 25 March 2020, 16:54:59 UTC | Update deps in opam file | 25 March 2020, 16:54:59 UTC |
| 8308954 | Yannick Forster | 25 March 2020, 16:53:22 UTC | remove a warning | 25 March 2020, 16:53:22 UTC |
| 0c0d47a | Yannick Forster | 25 March 2020, 16:26:36 UTC | Update travis | 25 March 2020, 16:26:36 UTC |
| 9fc277e | Yannick Forster | 25 March 2020, 16:24:32 UTC | port to 8.11 | 25 March 2020, 16:24:32 UTC |
| b9b3834 | Yannick Forster | 25 March 2020, 09:58:11 UTC | Fig global make targets | 25 March 2020, 09:58:11 UTC |
| b53b214 | Yannick Forster | 25 March 2020, 09:12:40 UTC | Fix travis file | 25 March 2020, 09:12:40 UTC |
| 137a367 | Yannick Forster | 25 March 2020, 08:33:29 UTC | Update README and opam file | 25 March 2020, 08:33:29 UTC |
| bef647d | Yannick Forster | 25 March 2020, 08:28:24 UTC | Update README | 25 March 2020, 08:28:24 UTC |
| 0de7d1c | Yannick Forster | 25 March 2020, 08:24:04 UTC | Fix versions in opam file | 25 March 2020, 08:24:04 UTC |
| ed09bee | Yannick Forster | 25 March 2020, 08:20:05 UTC | Removed submodules and updated opam file | 25 March 2020, 08:20:51 UTC |
| ed4ff57 | Yannick Forster | 24 March 2020, 18:14:33 UTC | Everything compiles under 8.10 | 24 March 2020, 18:14:33 UTC |
| 4481aea | Yannick Forster | 24 March 2020, 17:31:11 UTC | More changes for 8.10 | 24 March 2020, 17:31:11 UTC |
| 4c22f3d | Fabian Kunze | 24 March 2020, 16:14:55 UTC | Fixed bug bu changing undocumented tactical to another one | 24 March 2020, 16:14:55 UTC |
| c89ffe5 | Yannick Forster | 24 March 2020, 15:24:07 UTC | first steps in porting to 8.10 | 24 March 2020, 15:24:07 UTC |
| 0abe97a | Dominique Larchey-Wendling | 05 March 2020, 15:45:27 UTC | Merge pull request #37 from DmxLarchey/lmcs_ups changed name of lemma | 05 March 2020, 15:45:27 UTC |
| 599cb58 | Dominique Larchey-Wendling | 05 March 2020, 15:15:37 UTC | changed name of lemma | 05 March 2020, 15:15:37 UTC |
| 6bb9129 | Yannick Forster | 05 March 2020, 14:59:16 UTC | Merge pull request #36 from DmxLarchey/lmcs_ups Updates for the LMCS submission | 05 March 2020, 14:59:16 UTC |
| d80d1a8 | Dominique Larchey-Wendling | 05 March 2020, 12:54:14 UTC | Removed dependency on Equations for inverting vec and pos dependent types. Possibly inversion lemma for ra_ca_c should be properly laid out instead of hand hacking inversions on a per-need basis which clogs the code | 05 March 2020, 12:54:14 UTC |
| 57a48d0 | Dominique Larchey-Wendling | 05 March 2020, 10:30:39 UTC | changed the defs of H10 and H10Z to (pos n,pos 0) instead of (pos n,Empty_set) | 05 March 2020, 10:30:39 UTC |
| 1480669 | Dominique Larchey-Wendling | 04 March 2020, 14:43:25 UTC | Merge branch 'wip' into libs_update | 04 March 2020, 14:43:25 UTC |
| 462c3a4 | Yannick Forster | 04 March 2020, 08:47:33 UTC | Merge pull request #31 from uds-psl/more_dprm new version of the DPRM which shows all availalable equivalences | 04 March 2020, 08:47:33 UTC |
| 5c66f33 | Yannick Forster | 03 March 2020, 17:18:51 UTC | Merge pull request #33 from lgaeher/master Fix makefile and coqdoc compilation | 03 March 2020, 17:18:51 UTC |
| 28de3a4 | Yannick Forster | 03 March 2020, 17:18:20 UTC | Merge pull request #34 from DmxLarchey/cleanup_murec_compiler Cleanup murec compiler, faster compile | 03 March 2020, 17:18:20 UTC |
| 70f6378 | Yannick Forster | 03 March 2020, 17:17:56 UTC | Merge pull request #35 from yforster/remove_admits Remove all admits | 03 March 2020, 17:17:56 UTC |
| 83f7410 | Yannick Forster | 03 March 2020, 16:18:02 UTC | Remove admits | 03 March 2020, 16:19:37 UTC |
| ed1f939 | Yannick Forster | 03 March 2020, 10:40:12 UTC | remove axiom | 03 March 2020, 16:19:37 UTC |
| 19ba623 | Dominique Larchey-Wendling | 02 March 2020, 09:51:49 UTC | small updates | 02 March 2020, 09:51:49 UTC |
| 6a8aec1 | Dominique Larchey-Wendling | 01 March 2020, 23:14:18 UTC | changed Let in Local Definition in ra_mm_env. to avoid big environments than hinder the efficiency of the omega tactic | 01 March 2020, 23:14:18 UTC |
| ab9b33d | Lennard Gäher | 22 February 2020, 18:52:46 UTC | remove parse-comments flag from coqdoc as this breaks doc generation (seems to be a bug in coqdoc as 'unknown token' stuff should not happen according to its documentation?) | 22 February 2020, 18:52:46 UTC |
| d22f6f2 | Lennard Gäher | 22 February 2020, 18:50:55 UTC | fix makefile regression introduced by 6ddce394ca5bc2206f6e0e2bcecc0582e70fb6a3 | 22 February 2020, 18:50:55 UTC |
| 466d429 | Lennard Gäher | 22 February 2020, 18:03:30 UTC | fix html target in makefile | 22 February 2020, 18:03:30 UTC |
| d553555 | Dominique Larchey-Wendling | 14 February 2020, 20:56:02 UTC | reverted to vec_list_In | 14 February 2020, 20:56:02 UTC |
| 278820c | Dominique Larchey-Wendling | 14 February 2020, 18:02:20 UTC | more cleanup | 14 February 2020, 18:02:20 UTC |
| a96230d | Dominique Larchey-Wendling | 14 February 2020, 17:53:19 UTC | finished cleanup and merge | 14 February 2020, 17:53:19 UTC |
| 93972dc | Dominique Larchey-Wendling | 14 February 2020, 14:27:28 UTC | the git checkout informative_lift Shared did import whole files and did not perform a proper merge !!! I now have to cleanup the mess | 14 February 2020, 14:27:28 UTC |
| 5a7d71a | Dominique Larchey-Wendling | 14 February 2020, 12:06:23 UTC | a prime testing procedure and nxtprime reflection tactic a discussion about the shape of possible and impossible fractran RE predicates | 14 February 2020, 12:06:23 UTC |
| f6d4c4b | Dominique Larchey-Wendling | 13 February 2020, 22:54:16 UTC | added DPRM for unary predicates including fractran | 13 February 2020, 22:54:16 UTC |
| 8a3ceb3 | Dominique Larchey-Wendling | 11 February 2020, 13:54:48 UTC | new version of the DPRM which shows equivalence between the computational models of MM, µrec and the different variants of Diohantineness | 11 February 2020, 13:54:48 UTC |
| aec2f58 | Dominique Larchey-Wendling | 07 February 2020, 14:16:36 UTC | Merge pull request #29 from yforster/H10Z Reduction from H10 to H10Z | 07 February 2020, 14:16:36 UTC |
| 605fa43 | Dominique Larchey-Wendling | 07 February 2020, 13:04:14 UTC | redefined H10Z as P(x1,...,xn) = 0%Z and removed dependency over Equations for depelim the pos lib already has inversion for pos (S n) as the tactic "invert pos p" some cleanup as well | 07 February 2020, 13:04:14 UTC |
| e0b41e6 | Yannick Forster | 07 February 2020, 11:38:47 UTC | Reduction from H10 to H10Z | 07 February 2020, 11:38:47 UTC |
| d552a7f | Yannick Forster | 06 February 2020, 17:42:03 UTC | Merge pull request #22 from uds-psl/better_bezout_extraction Construction of an H10C-universal µ-recursive function | 06 February 2020, 17:42:03 UTC |
| 468a538 | Dominique Larchey-Wendling | 06 February 2020, 14:55:18 UTC | Merge branch 'master' into better_bezout_extraction resync with updated master | 06 February 2020, 14:55:18 UTC |
| 9dddee6 | Yannick Forster | 06 February 2020, 13:25:32 UTC | Merge pull request #28 from yforster/mu_to_lambda Mu to lambda | 06 February 2020, 13:25:32 UTC |
| c10a31c | Yannick Forster | 06 February 2020, 09:04:54 UTC | Merge remote-tracking branch 'origin/master' into mu_to_lambda | 06 February 2020, 09:04:54 UTC |
| 98cecb0 | Yannick Forster | 06 February 2020, 09:03:04 UTC | Merge pull request #26 from DmxLarchey/h10_journal A fork for smoother reduction dio_form -> dio_elem | 06 February 2020, 09:03:04 UTC |
| 2ef5eeb | Yannick Forster | 05 February 2020, 16:41:58 UTC | Added reduction from mu_halting to lambda calculus | 05 February 2020, 16:41:58 UTC |
| 91a93c4 | Yannick Forster | 04 February 2020, 11:54:14 UTC | progress | 04 February 2020, 11:54:14 UTC |
