| ddeab06 | Yishuai Li | 17 January 2020, 19:16:34 UTC | Notation ;; should be right associative | 17 January 2020, 21:01:03 UTC |
| 0b0c82b | Yishuai Li | 16 January 2020, 18:32:39 UTC | Core: fix compilation in Decision | 16 January 2020, 18:32:39 UTC |
| ef18c1d | Gregory Malecha | 16 January 2020, 18:23:35 UTC | Cleaner implementation of decideP | 16 January 2020, 18:23:35 UTC |
| 70d2f8c | Abhishek Anand (optiplex7010@home) | 16 January 2020, 16:38:48 UTC | comment about borrowing names from SF and the (dis)similarities in the implementation | 16 January 2020, 16:38:48 UTC |
| 01d8892 | Yishuai Li | 15 January 2020, 20:03:03 UTC | Merge branch 'master' into squiggleeq | 15 January 2020, 20:03:03 UTC |
| b6ac762 | Yishuai Li | 10 January 2020, 02:59:40 UTC | Update templates | 10 January 2020, 03:02:37 UTC |
| f258f27 | Yishuai Li | 08 January 2020, 00:43:14 UTC | Uncomment MonadLaws | 09 January 2020, 19:49:10 UTC |
| ee71d14 | Yishuai Li | 07 January 2020, 23:26:24 UTC | Remove P* | 09 January 2020, 19:49:10 UTC |
| 110ca2e | Yishuai Li | 26 December 2019, 22:24:48 UTC | Update notations | 09 January 2020, 19:49:10 UTC |
| 9d5d1d3 | Abhishek Anand (optiplex7010@home) | 08 January 2020, 00:57:41 UTC | better naming | 08 January 2020, 00:57:41 UTC |
| 9399778 | Abhishek Anand (optiplex7010@home) | 07 January 2020, 22:50:24 UTC | fixed indentation | 07 January 2020, 22:50:24 UTC |
| 89e8253 | Abhishek Anand (optiplex7010@home) | 07 January 2020, 22:40:04 UTC | a more reliable implementation of hyp hiding. moved to another file | 07 January 2020, 22:40:04 UTC |
| 05533df | Abhishek Anand (optiplex7010@home) | 07 January 2020, 21:00:43 UTC | generic stuff from squiggleeq: fwd tactics and decision helpers | 07 January 2020, 21:00:43 UTC |
| d3b7f4e | Yishuai Li | 25 December 2019, 21:20:48 UTC | Generic Makefile for CoqdocJs | 25 December 2019, 21:20:48 UTC |
| a21585d | Yishuai Li | 25 December 2019, 01:19:55 UTC | Vanilla CoqdocJs | 25 December 2019, 20:59:46 UTC |
| d97d562 | Yishuai Li | 22 December 2019, 03:28:46 UTC | Applicative is Functor | 22 December 2019, 03:28:46 UTC |
| 8e1713c | Jason Gross | 25 November 2019, 19:39:10 UTC | Make vector template-polymorphic again After coq/coq#9918, vector was no-longer template polymorphic. This backwards-compatible commit fixes that. | 04 December 2019, 01:16:58 UTC |
| 341323a | Yishuai Li | 22 November 2019, 18:55:29 UTC | [ci skip] update template | 22 November 2019, 18:55:29 UTC |
| 93eebe8 | Yishuai Li | 17 November 2019, 22:00:42 UTC | Extras: add curry and related lemmas | 17 November 2019, 22:00:42 UTC |
| d8fce97 | Yishuai Li | 29 October 2019, 22:52:39 UTC | CI test dependants | 08 November 2019, 20:53:25 UTC |
| 9ad8341 | Yishuai Li | 19 October 2019, 05:05:26 UTC | Documentation for v0.10.3 README from modified mustache | 19 October 2019, 05:05:45 UTC |
| ad61bb3 | Yishuai Li | 17 October 2019, 02:23:41 UTC | Add v0.10.2 documentation | 17 October 2019, 02:23:41 UTC |
| 0eece0d | Yishuai Li | 14 October 2019, 21:45:35 UTC | Deploy GitHub pages | 15 October 2019, 04:36:14 UTC |
| dfe8332 | Yishuai Li | 14 October 2019, 21:31:56 UTC | Generate documentation | 15 October 2019, 04:06:41 UTC |
| 847e037 | Yishuai Li | 14 October 2019, 20:36:30 UTC | OPAM: light-uninstall is needless | 14 October 2019, 20:40:48 UTC |
| 5919904 | Théo Zimmermann | 14 October 2019, 12:39:34 UTC | Fix CircleCI badge after move to coq-community. | 14 October 2019, 12:39:34 UTC |
| c99c58a | Yishuai Li | 13 October 2019, 21:15:50 UTC | Add meta.yml; update README and opam | 13 October 2019, 21:16:03 UTC |
| 8530e43 | Yishuai Li | 11 October 2019, 00:23:02 UTC | CI build locally | 11 October 2019, 00:33:03 UTC |
| fa2b375 | Yishuai Li | 10 October 2019, 02:04:27 UTC | CI status badge | 11 October 2019, 00:01:40 UTC |
| b1fe2bb | Lysxia | 26 September 2019, 18:44:24 UTC | Makefile: improve clean command | 10 October 2019, 11:33:45 UTC |
| 02d4c65 | Yishuai Li | 10 October 2019, 01:40:00 UTC | CircleCI is better than Travis | 10 October 2019, 01:43:45 UTC |
| d683ad1 | Lysxia | 10 October 2019, 01:13:45 UTC | Comment out eq_list_eq (workaround #73) | 10 October 2019, 01:15:28 UTC |
| 672e63a | Lysxia | 09 October 2019, 21:09:25 UTC | Replace section annotations with global Set Universe Polymorphism | 09 October 2019, 22:53:35 UTC |
| e800d3e | Gregory Malecha | 22 July 2019, 11:21:37 UTC | Merge pull request #65 from ppedrot/static-poly-section Fix w.r.t. coq/coq#10441. | 22 July 2019, 11:21:37 UTC |
| 30d6200 | Pierre-Marie Pédrot | 27 June 2019, 18:53:33 UTC | Fix w.r.t. coq/coq#10441. | 11 July 2019, 09:43:45 UTC |
| f53ffbf | Gregory Malecha | 08 July 2019, 01:49:30 UTC | Merge pull request #68 from jbaum98/master Fix inconsistent notation levels associativity | 08 July 2019, 01:49:30 UTC |
| 433fcc1 | Jake Waksbaum | 07 July 2019, 23:34:35 UTC | Fix inconsistent notation levels associativity Declaring two notations with different associativities but the same precedence level leads to a conflict. Instead we establish the convention that even precedence levels are for left-associative notations, and odd precedence levels are for right-associative notations. | 07 July 2019, 23:37:20 UTC |
| 5dc7ac2 | Gregory Malecha | 05 July 2019, 10:59:18 UTC | Merge pull request #67 from maximedenes/fix-export-bug Avoid relying on `Export` bug | 05 July 2019, 10:59:18 UTC |
| 66623d9 | Maxime Dénès | 05 July 2019, 08:58:33 UTC | Avoid relying on `Export` bug See https://github.com/coq/coq/issues/10474 | 05 July 2019, 08:58:33 UTC |
| 32d42e9 | Gregory Malecha | 01 July 2019, 02:22:02 UTC | Merge pull request #63 from vzaliva/comonads Comonads | 01 July 2019, 02:22:02 UTC |
| 1c5095b | Gregory Malecha | 25 June 2019, 02:02:53 UTC | Merge pull request #64 from coq-ext-lib/finite-map-remove-facts Finite map facts about remove | 25 June 2019, 02:02:53 UTC |
| 5ab128b | Gregory Malecha | 25 June 2019, 02:01:06 UTC | remove facts for finite maps. | 25 June 2019, 02:01:06 UTC |
| f179136 | Vadim Zaliva | 26 May 2019, 17:36:40 UTC | `coret` and `cobind` aliases | 26 May 2019, 17:36:40 UTC |
| ca25b49 | Vadim Zaliva | 26 May 2019, 17:09:54 UTC | Merge remote-tracking branch 'upstream/master' into comonads | 26 May 2019, 17:09:54 UTC |
| f27a18a | Gregory Malecha | 20 May 2019, 20:42:44 UTC | Merge pull request #62 from liyishuai/assoc Make <$> and <*> left associative | 20 May 2019, 20:42:44 UTC |
| 15900db | Yishuai Li | 20 May 2019, 20:40:49 UTC | Make <$> and <*> left associative fix #61 | 20 May 2019, 20:40:53 UTC |
| c0c934c | Gregory Malecha | 29 March 2019, 13:48:38 UTC | Merge pull request #60 from Lysxia/implicit-arg-monads Implicit arguments for mkOptionT, mkEitherT, mkIdentT | 29 March 2019, 13:48:38 UTC |
| cf6b3a4 | Lysxia | 28 March 2019, 13:48:42 UTC | Implicit arguments for mkOptionT, mkEitherT, mkIdentT | 28 March 2019, 13:48:42 UTC |
| ca87e9e | Gregory Malecha | 17 March 2019, 20:55:19 UTC | Merge pull request #59 from liyishuai/ci Travis CI | 17 March 2019, 20:55:19 UTC |
| faaf30d | Yishuai Li | 15 March 2019, 14:48:40 UTC | Travis CI | 15 March 2019, 18:29:25 UTC |
| 355320e | Gregory Malecha | 15 March 2019, 18:06:51 UTC | Merge pull request #58 from liyishuai/mkStateT-arguments StateMonad: implicit arguments for mkStateT | 15 March 2019, 18:06:51 UTC |
| 0660941 | Yishuai Li | 15 March 2019, 14:33:41 UTC | StateMonad: implicit arguments for mkStateT | 15 March 2019, 14:33:41 UTC |
| e7dbf45 | Gregory Malecha | 22 February 2019, 02:24:29 UTC | Merge pull request #57 from Lysxia/seq-assoc Make >=> right associative | 22 February 2019, 02:24:29 UTC |
| 7db5188 | Lysxia | 22 February 2019, 00:58:25 UTC | Move right associative monadic notations to level 60 | 22 February 2019, 00:58:25 UTC |
| 235d996 | Lysxia | 21 February 2019, 19:58:24 UTC | Make >=> right associative | 21 February 2019, 19:58:24 UTC |
| a502568 | Gregory Malecha | 05 February 2019, 03:33:14 UTC | fix deprecated warnings. | 05 February 2019, 03:33:14 UTC |
| 3acee34 | Gregory Malecha | 01 February 2019, 11:55:24 UTC | Merge pull request #54 from Mbodin/master Adding a way to convert [member]s into [In]s. | 01 February 2019, 11:55:24 UTC |
| 915a186 | Martin Bodin | 01 February 2019, 10:19:34 UTC | Adding a way to convert [member]s into [In]s. | 01 February 2019, 10:19:34 UTC |
| adc7c70 | Gregory Malecha | 31 January 2019, 16:11:43 UTC | Merge pull request #53 from Mbodin/master Adding functions to go from lists to hlists and conversely. | 31 January 2019, 16:11:43 UTC |
| 5c1a99c | Martin Bodin | 31 January 2019, 14:25:43 UTC | Unfolding [hlist_gen_member]. | 31 January 2019, 14:25:43 UTC |
| 180a4ac | Martin Bodin | 31 January 2019, 12:35:14 UTC | From [hlist] to [Forall] (lacking a [Proper] instance). | 31 January 2019, 12:35:14 UTC |
| 7238721 | Martin Bodin | 31 January 2019, 11:42:09 UTC | A (bad) [Proper] instance for [equiv_hlist_gen]. | 31 January 2019, 11:42:09 UTC |
| 9ed5d84 | Martin Bodin | 31 January 2019, 11:22:10 UTC | Adding a version of [hlist_gen] taking [member a ls] as argument. | 31 January 2019, 11:22:10 UTC |
| 3986a0c | Martin Bodin | 31 January 2019, 11:06:59 UTC | Putting [hlist_gen] into a section. | 31 January 2019, 11:06:59 UTC |
| 1a2def0 | Martin Bodin | 30 January 2019, 17:41:44 UTC | Adding a [Proper] instance. | 30 January 2019, 17:41:44 UTC |
| 0f4eb4e | Martin Bodin | 30 January 2019, 17:21:21 UTC | Some arguments of [hlist_gen] are now implicit ad maximally inserted. | 30 January 2019, 17:22:37 UTC |
| c1bae69 | Martin Bodin | 30 January 2019, 15:12:01 UTC | Adding functions to go from lists to hlists and conversely. | 30 January 2019, 15:12:01 UTC |
| 5f5c4e6 | Gregory Malecha | 24 January 2019, 06:27:09 UTC | Merge pull request #52 from maximedenes/instance-nobody-open-proof Make trivial instances explicit | 24 January 2019, 06:27:09 UTC |
| 90a2565 | Maxime Dénès | 24 January 2019, 00:03:20 UTC | Make trivial instances explicit This is in preparation for coq/coq#9274. | 24 January 2019, 00:03:20 UTC |
| 534e4e9 | Gregory Malecha | 23 December 2018, 12:28:11 UTC | Merge pull request #51 from maximedenes/no-refine-instance Do not rely on `Refine Instance Mode` | 23 December 2018, 12:28:11 UTC |
| bb316c4 | Maxime Dénès | 23 December 2018, 08:43:11 UTC | Do not rely on `Refine Instance Mode` This option is soon going to be turned off by default. See https://github.com/coq/coq/pull/9270 | 23 December 2018, 08:43:11 UTC |
| e49214f | Gregory Malecha | 13 November 2018, 22:41:44 UTC | Merge pull request #49 from coq-ext-lib/string-fold-direction Fixing the fold direction for string to be consistent with list | 13 November 2018, 22:41:44 UTC |
| 3845f96 | Gregory Malecha | 13 November 2018, 22:34:08 UTC | fixing the fold direction for string to be consistent with list | 13 November 2018, 22:34:08 UTC |
| f2d4360 | Gregory Malecha | 09 November 2018, 22:44:49 UTC | Merge pull request #47 from SkySkimmer/fix-alg-univ Remove algebraic universes in match return clauses. | 09 November 2018, 22:44:49 UTC |
| a0a43d1 | Gaëtan Gilbert | 09 November 2018, 14:43:43 UTC | Remove algebraic universes in match return clauses. We have to use explicit universes in order to avoid having additional floating universes. | 09 November 2018, 14:43:43 UTC |
| 14e7d88 | Gregory Malecha | 21 October 2018, 22:46:41 UTC | Merge pull request #46 from Lysxia/master Display the new ' _ <- _ ;; _ notation only with nontrivial patterns | 21 October 2018, 22:46:41 UTC |
| e7a00b3 | Gregory Malecha | 21 October 2018, 22:46:15 UTC | Merge pull request #42 from maximedenes/omega-lia Prepare for porting to lia | 21 October 2018, 22:46:15 UTC |
| 174889d | Gregory Malecha | 21 October 2018, 22:45:43 UTC | Merge pull request #44 from vzaliva/mcompose added monadic composition operator `>=>` | 21 October 2018, 22:45:43 UTC |
| 3ce4007 | Lysxia | 21 October 2018, 15:42:21 UTC | Display the new ' _ <- _ ;; _ notation only with nontrivial patterns | 21 October 2018, 15:42:21 UTC |
| 548c861 | Gregory Malecha | 17 October 2018, 15:17:13 UTC | fixing a bug in the state monad. | 17 October 2018, 15:17:13 UTC |
| b480c83 | Vadim Zaliva | 14 October 2018, 02:55:56 UTC | defined `mcompose` | 14 October 2018, 02:55:56 UTC |
| c986741 | Vadim Zaliva | 13 October 2018, 02:07:13 UTC | added monadic composition operator `>=>` | 13 October 2018, 02:07:13 UTC |
| f911376 | Maxime Dénès | 26 July 2018, 13:24:20 UTC | Prepare for porting to lia This backward-compatible patch prepares ext-lib for https://github.com/coq/coq/pull/7878 | 26 July 2018, 13:25:25 UTC |
| a9c1389 | Gregory Malecha | 14 July 2018, 21:59:39 UTC | Merge pull request #41 from coq-ext-lib/v8.8 V8.8 | 14 July 2018, 21:59:39 UTC |
| 5dd9cfa | Gregory Malecha | 30 June 2018, 02:28:08 UTC | Merge pull request #40 from Lysxia/v8.8 Add Monad notation to bind patterns | 30 June 2018, 02:28:08 UTC |
| a3af071 | Lysxia | 29 June 2018, 22:25:34 UTC | Add Monad notation to bind patterns | 29 June 2018, 22:48:03 UTC |
| 293dbd1 | Gregory Malecha | 30 April 2018, 06:58:10 UTC | Merge branch 'v8.8' | 30 April 2018, 06:58:10 UTC |
| a105855 | Gregory Malecha | 29 April 2018, 22:18:49 UTC | remove warnings in Coq 8.8 | 29 April 2018, 22:18:49 UTC |
| b8f7334 | Gregory Malecha | 18 November 2017, 03:19:31 UTC | compatability with coq 8.7 | 18 November 2017, 03:19:31 UTC |
| 974a79e | Gregory Malecha | 22 April 2017, 22:02:18 UTC | Merge pull request #36 from coq-ext-lib/vzaliva-v8.6-writer a few cosmetic changes to mapWriterT, etc. | 22 April 2017, 22:02:18 UTC |
| c72be4e | Gregory Malecha | 22 April 2017, 22:00:44 UTC | Merge pull request #34 from vzaliva/v8.6-writer mapWriter, castWriter | 22 April 2017, 22:00:44 UTC |
| c562d4f | Gregory Malecha | 22 April 2017, 21:56:37 UTC | a few cosmetic cleanups. | 22 April 2017, 21:56:37 UTC |
| 500f04d | Vadim Zaliva | 22 April 2017, 17:23:04 UTC | Changed arguments' order per Gregory suggestion | 22 April 2017, 17:23:04 UTC |
| 0a08d4e | Vadim Zaliva | 22 April 2017, 00:21:16 UTC | mapWriter, castWriter | 22 April 2017, 00:21:16 UTC |
| e065b13 | Vadim Zaliva | 09 March 2017, 22:29:07 UTC | CoMonadLaws class | 09 March 2017, 22:29:07 UTC |
| cfd0fc3 | Vadim Zaliva | 09 March 2017, 22:20:25 UTC | renamed CoMonad functoins coret and cobind to match names (extract,extend) and argument order used in Haskell and other places | 09 March 2017, 22:20:25 UTC |
| 5d19dff | Gregory Malecha | 06 January 2017, 03:04:11 UTC | delete Makefile.coq on clean. | 06 January 2017, 03:04:11 UTC |
| e5e5831 | Gregory Malecha | 06 January 2017, 02:50:09 UTC | building on 8.6 | 06 January 2017, 02:50:09 UTC |
| d8d0bb3 | Gregory Malecha | 29 October 2016, 22:40:40 UTC | simplify universes in Hlist. | 29 October 2016, 22:41:02 UTC |
| ac34e1f | Gregory Malecha | 16 July 2016, 19:42:17 UTC | Merge pull request #28 from JasonGross/patch-2 Respect COQBIN on calling coq_makefile (examples) | 16 July 2016, 19:42:17 UTC |
