| ea6b280 | Gregory Malecha | 11 February 2016, 17:48:21 UTC | a few more functions. | 11 February 2016, 17:48:41 UTC |
| 839d5b6 | Gregory Malecha | 04 February 2016, 23:55:59 UTC | Merge pull request #20 from vzaliva/StateGame-example State game example | 04 February 2016, 23:55:59 UTC |
| 4027ca0 | Vadim Zaliva | 04 February 2016, 23:30:55 UTC | Updated per Gregory suggestions. | 04 February 2016, 23:30:55 UTC |
| 34b1ac7 | Vadim Zaliva | 04 February 2016, 05:42:49 UTC | Simple example of using StateMonad. | 04 February 2016, 05:42:49 UTC |
| 811b3b0 | Gregory Malecha | 02 February 2016, 07:09:58 UTC | Update README.md | 02 February 2016, 07:09:58 UTC |
| 524489b | Ben | 06 January 2016, 19:06:17 UTC | Fix typo | 25 January 2016, 19:11:06 UTC |
| cc65518 | jesper-bengtson | 22 January 2016, 21:49:03 UTC | made all functions in PList.v univerese polymorphic. | 22 January 2016, 21:49:03 UTC |
| 3e4d65f | jesper-bengtson | 22 January 2016, 21:40:22 UTC | Added In, anyb and allb to PList.v | 22 January 2016, 21:40:22 UTC |
| b6f6bab | Gregory Malecha | 22 January 2016, 19:48:18 UTC | Merge branch 'v8.5-trunk' into v8.5 | 22 January 2016, 19:48:18 UTC |
| 2cf7efc | Gregory Malecha | 18 January 2016, 21:17:40 UTC | missing file. | 18 January 2016, 21:17:40 UTC |
| 058fa44 | Gregory Malecha | 18 January 2016, 18:07:34 UTC | adding a transparent version of UIP - The proof is based on Bruno's proof in the standard library. | 18 January 2016, 18:07:34 UTC |
| d8b51b6 | Gregory Malecha | 17 December 2015, 06:07:40 UTC | vector_In | 17 December 2015, 06:07:40 UTC |
| 9b4e818 | Gregory Malecha | 17 December 2015, 05:48:23 UTC | adding vector_map and vector_dec. | 17 December 2015, 05:48:23 UTC |
| b4b6057 | Gregory Malecha | 16 December 2015, 00:53:57 UTC | adding a lazy-man's constructor for RelDec | 16 December 2015, 00:53:57 UTC |
| e57362a | Gregory Malecha | 16 December 2015, 00:28:22 UTC | intuition is introducing an axiom in List. | 16 December 2015, 00:28:22 UTC |
| 8c8ccb9 | Gregory Malecha | 08 December 2015, 01:38:06 UTC | polymorphic definitions for basic data types. | 08 December 2015, 01:41:02 UTC |
| af86e9c | Guillaume Claret | 26 November 2015, 17:36:17 UTC | OPAM installation instructions | 08 December 2015, 01:40:20 UTC |
| 0ba36ff | Gregory Malecha | 09 November 2015, 17:36:55 UTC | fixing broken Makefile. | 09 November 2015, 17:36:55 UTC |
| c3f2d7d | Gregory Malecha | 09 November 2015, 17:19:09 UTC | no longer need -type-in-type in the examples. | 09 November 2015, 17:33:33 UTC |
| 29e9a04 | Gregory Malecha | 20 October 2015, 23:15:31 UTC | fixing issue #13 | 09 November 2015, 17:33:33 UTC |
| ccc528a | Gregory Malecha | 17 October 2015, 22:22:34 UTC | fixes to compile with 8.5-tip | 09 November 2015, 17:33:33 UTC |
| be88458 | Gregory Malecha | 13 October 2015, 00:04:34 UTC | removing -type-in-type. | 09 November 2015, 17:33:30 UTC |
| 5a4c2c3 | Gregory Malecha | 02 September 2015, 00:42:51 UTC | adding missing file. | 09 November 2015, 17:33:11 UTC |
| 69c3358 | Gregory Malecha | 30 July 2015, 19:20:32 UTC | adding OutOf. | 09 November 2015, 17:33:11 UTC |
| 6fd67e6 | Gregory Malecha | 29 July 2015, 22:06:06 UTC | Better 'Into' function for SumN | 09 November 2015, 17:33:11 UTC |
| 89ea418 | Gregory Malecha | 28 July 2015, 22:50:30 UTC | fixing building of examples and some List theorems. | 09 November 2015, 17:33:09 UTC |
| 031d0db | Gregory Malecha | 21 July 2015, 19:27:40 UTC | SumN is injective. | 09 November 2015, 17:30:56 UTC |
| 54ae85c | jesper-bengtson | 16 July 2015, 21:26:58 UTC | Added OneOf_Empty | 09 November 2015, 17:30:56 UTC |
| fbcdadd | jesper-bengtson | 10 July 2015, 14:35:36 UTC | Slight changes on maps | 09 November 2015, 17:30:56 UTC |
| f2f4068 | Gregory Malecha | 03 July 2015, 04:14:50 UTC | fixing a bug in Data.Fin. | 09 November 2015, 17:30:56 UTC |
| 9588b93 | Gregory Malecha | 09 November 2015, 04:51:21 UTC | porting of most things so that it builds with 8.5~beta3 | 09 November 2015, 04:51:21 UTC |
| e7233b6 | Gregory Malecha | 30 June 2015, 05:00:16 UTC | the "right" way to do Makefiles. Conflicts: _CoqProject | 09 November 2015, 01:40:27 UTC |
| ad3e508 | Gregory Malecha | 09 November 2015, 01:36:59 UTC | working on porting to 8.5 beta 3 | 09 November 2015, 01:36:59 UTC |
| 9e72791 | Gregory Malecha | 30 June 2015, 16:49:34 UTC | updates to work with coq-8.5 (trunk) | 30 June 2015, 16:49:34 UTC |
| 138c915 | Gregory Malecha | 31 May 2015, 01:44:38 UTC | fixing some of the examples. | 31 May 2015, 01:44:38 UTC |
| 8b7bbc7 | Gregory Malecha | 31 May 2015, 01:32:51 UTC | fixing imports and changing to _CoqProject. | 31 May 2015, 01:32:51 UTC |
| 4a30036 | Gregory Malecha | 22 May 2015, 20:48:09 UTC | some more polymorphism. | 22 May 2015, 20:48:09 UTC |
| 4c3ad63 | Gregory Malecha | 22 May 2015, 19:21:55 UTC | a bit more polymorphism. | 22 May 2015, 19:21:55 UTC |
| 87f6e9d | Gregory Malecha | 21 May 2015, 21:57:04 UTC | some more universes - punting on some of the laws. | 21 May 2015, 21:57:04 UTC |
| 3b2e007 | Gregory Malecha | 21 May 2015, 16:49:35 UTC | making monads universe polymorphic. - this still is not optimal. | 21 May 2015, 16:49:35 UTC |
| 9f605f7 | Gregory Malecha | 07 May 2015, 20:58:57 UTC | fixing a bit of the Makefile. | 07 May 2015, 20:58:57 UTC |
| 94d71bf | Gregory Malecha | 07 April 2015, 17:23:39 UTC | fixes. | 07 April 2015, 17:23:39 UTC |
| b818cb8 | Gregory Malecha | 07 April 2015, 17:21:03 UTC | Merge branch '8.5' of github.com:coq-ext-lib/coq-ext-lib into 8.5 | 07 April 2015, 17:21:03 UTC |
| a0323dc | Gregory Malecha | 11 February 2015, 02:52:56 UTC | autorewrite is not as useful with the 8.5 beta. | 07 April 2015, 17:20:49 UTC |
| c18aa40 | Gregory Malecha | 10 February 2015, 22:08:20 UTC | support for 8.5 | 07 April 2015, 17:20:49 UTC |
| 9d7c744 | Gregory Malecha | 03 April 2015, 06:49:30 UTC | a few more lemmas for Data.Prop. | 03 April 2015, 06:49:30 UTC |
| 49778e3 | Gregory Malecha | 03 April 2015, 06:20:20 UTC | A few more proofs. | 03 April 2015, 06:24:35 UTC |
| baad05d | Gregory Malecha | 11 February 2015, 02:52:56 UTC | autorewrite is not as useful with the 8.5 beta. | 11 February 2015, 02:52:56 UTC |
| 35fae8a | Gregory Malecha | 10 February 2015, 22:08:20 UTC | support for 8.5 | 10 February 2015, 22:08:20 UTC |
| ac569fb | gregory malecha | 08 January 2015, 00:37:53 UTC | printString in the printing example. | 08 January 2015, 00:37:53 UTC |
| bd1caa9 | Gregory Malecha | 07 January 2015, 03:15:41 UTC | a simple example for printing. | 07 January 2015, 03:15:41 UTC |
| ab28e47 | Gregory Malecha | 06 December 2014, 04:29:42 UTC | adding eq_sym_eq_sym to Data.Eq. | 06 December 2014, 04:29:42 UTC |
| 229e122 | Gregory Malecha | 14 November 2014, 06:15:28 UTC | moving some lemmas. | 14 November 2014, 06:15:28 UTC |
| 1278812 | Gregory Malecha | 06 November 2014, 03:45:42 UTC | adding lazy list. | 06 November 2014, 03:45:42 UTC |
| 442c7e0 | Gregory Malecha | 05 November 2014, 18:55:29 UTC | more consistent naming in Data.Prop. | 05 November 2014, 18:55:29 UTC |
| c32e340 | Gregory Malecha | 05 November 2014, 18:33:32 UTC | more definitions! | 05 November 2014, 18:33:32 UTC |
| b5e3433 | Gregory Malecha | 03 November 2014, 05:29:35 UTC | injective instances for List. | 03 November 2014, 05:29:35 UTC |
| 5faa035 | Gregory Malecha | 21 October 2014, 20:29:25 UTC | Merge branch 'master' of github.com:coq-ext-lib/coq-ext-lib | 21 October 2014, 20:29:25 UTC |
| fae710a | Gregory Malecha | 21 October 2014, 20:29:12 UTC | example of monad reasoning. | 21 October 2014, 20:29:12 UTC |
| c2c71a2 | Gregory Malecha | 09 October 2014, 12:31:37 UTC | Merge pull request #8 from clarus/master Bug fixes for conversions from integers to strings. | 09 October 2014, 12:31:37 UTC |
| 56295f9 | Guillaume Claret | 09 October 2014, 11:04:12 UTC | digit2ascii function fixed | 09 October 2014, 11:04:12 UTC |
| 0039176 | Guillaume Claret | 09 October 2014, 11:03:40 UTC | nat2string function fixed | 09 October 2014, 11:03:40 UTC |
| f6da121 | Gregory Malecha | 05 October 2014, 03:19:38 UTC | modifying the definition of equivalence of options. | 05 October 2014, 03:19:38 UTC |
| c8826ea | Gregory Malecha | 28 September 2014, 23:20:31 UTC | implementation of SumN. | 28 September 2014, 23:20:31 UTC |
| 0fe7953 | Gregory Malecha | 22 September 2014, 02:40:32 UTC | hrel and flip | 22 September 2014, 02:40:32 UTC |
| cf21029 | Gregory Malecha | 19 September 2014, 20:01:29 UTC | heterogenous relatedness when the relations are the same implies homogeneous relatedness | 19 September 2014, 20:01:29 UTC |
| f2cfd3e | Gregory Malecha | 19 September 2014, 19:57:46 UTC | heterogeneous relations on hlists | 19 September 2014, 19:57:46 UTC |
| 1b16f84 | Gregory Malecha | 19 September 2014, 17:25:38 UTC | lemmas about equiv_hlist. | 19 September 2014, 17:25:38 UTC |
| 28b4161 | Gregory Malecha | 18 September 2014, 19:35:11 UTC | implicit arguments to mapT_list. | 18 September 2014, 19:35:11 UTC |
| d8d091f | Gregory Malecha | 18 September 2014, 17:34:14 UTC | cleaner definition of list traverse | 18 September 2014, 17:34:14 UTC |
| a535a93 | Gregory Malecha | 15 September 2014, 00:52:22 UTC | implementation of Sum. | 15 September 2014, 00:52:22 UTC |
| 5c27c83 | Gregory Malecha | 12 September 2014, 20:26:22 UTC | Equational reasoning for Prop in Data.Prop | 12 September 2014, 20:26:22 UTC |
| 8e54e77 | Gregory Malecha | 07 August 2014, 02:04:20 UTC | Dead code in Data.Prop. | 07 August 2014, 02:04:20 UTC |
| e361819 | Gregory Malecha | 06 August 2014, 20:28:38 UTC | this is not provable without decidable equality. | 06 August 2014, 20:28:38 UTC |
| 47d1155 | Gregory Malecha | 01 August 2014, 22:15:37 UTC | Remove ListNth's and Show's dependence on omega. | 01 August 2014, 22:15:37 UTC |
| e04ba49 | Gregory Malecha | 01 August 2014, 20:30:08 UTC | don't add a rewrite for symmetry. | 01 August 2014, 20:30:08 UTC |
| 28cafe6 | Gregory Malecha | 01 August 2014, 19:33:38 UTC | Clean up for some eq_ lemmas - eq_option_eq moved to Data.Option - eq_list_eq added to Data.List - Changed Tactics.Equality to contain rewrites for Data.Eq - Building rewrite database for eq_matches | 01 August 2014, 19:33:38 UTC |
| 3ba620d | Gregory Malecha | 30 July 2014, 00:07:22 UTC | Removing EqDec requirements from Hcons inversion. | 30 July 2014, 00:07:22 UTC |
| 78d4433 | Gregory Malecha | 28 July 2014, 15:54:19 UTC | "f_equal" for matches. | 28 July 2014, 15:54:19 UTC |
| d4fe117 | Gregory Malecha | 28 July 2014, 15:53:57 UTC | adding injective instance for S | 28 July 2014, 15:53:57 UTC |
| 42d55a5 | Gregory Malecha | 18 July 2014, 23:26:49 UTC | Lemmas about matching on pf and then eq_sym pf. | 18 July 2014, 23:26:49 UTC |
| 370994c | Gregory Malecha | 08 July 2014, 13:23:44 UTC | remove EqDec requirement for hlist_nth_hlist_app - transparent proofs make all the difference. | 08 July 2014, 13:23:44 UTC |
| 7c5ce6c | Gregory Malecha | 18 June 2014, 17:09:49 UTC | Fun is an applicative. | 18 June 2014, 17:09:49 UTC |
| bf4e713 | Gregory Malecha | 18 June 2014, 03:53:16 UTC | well_founded relations are Irreflexive | 18 June 2014, 03:53:16 UTC |
| 5d9238a | Gregory Malecha | 14 June 2014, 22:17:51 UTC | change_rewrite | 14 June 2014, 22:17:51 UTC |
| b2303cd | Gregory Malecha | 10 June 2014, 17:15:48 UTC | Adding nth_error_length_lt = Fixing imports | 10 June 2014, 17:15:48 UTC |
| d912f9c | Gregory Malecha | 29 May 2014, 14:19:02 UTC | Adding ExtLib.Data.Member. - One proof seems to require UIP_refl, perhaps there is a way around this? | 29 May 2014, 14:19:02 UTC |
| 338dfc1 | Gregory Malecha | 26 May 2014, 13:57:59 UTC | lemmas for manipulating matches on eq. | 26 May 2014, 13:57:59 UTC |
| a7a437e | Gregory Malecha | 08 May 2014, 19:44:42 UTC | a more useful hlist_app_nil_r. | 08 May 2014, 19:44:42 UTC |
| 5427df3 | Gregory Malecha | 08 May 2014, 18:52:52 UTC | hlist_app_nil_r. | 08 May 2014, 18:52:52 UTC |
| 95de1b3 | Gregory Malecha | 07 May 2014, 23:04:21 UTC | removing some dependence on decidable equality. | 07 May 2014, 23:04:21 UTC |
| 9fe9db6 | Gregory Malecha | 30 April 2014, 02:00:05 UTC | Merge branch 'master' of github.com:coq-ext-lib/coq-ext-lib | 30 April 2014, 02:00:05 UTC |
| 7752939 | Gregory Malecha | 30 April 2014, 01:59:16 UTC | removing an old comment. | 30 April 2014, 01:59:16 UTC |
| 695e176 | gregory malecha | 28 April 2014, 03:19:47 UTC | adding FunctorLaws. | 28 April 2014, 03:19:47 UTC |
| 9f2ce47 | Gregory Malecha | 09 April 2014, 21:33:21 UTC | starting to make consistent with coq trunk. | 09 April 2014, 21:33:21 UTC |
| c18fee9 | Gregory Malecha | 06 April 2014, 16:21:32 UTC | working on what match means. | 06 April 2014, 16:21:32 UTC |
| 8b39fdd | Gregory Malecha | 05 April 2014, 16:27:41 UTC | Improvements to Data to support dependency | 05 April 2014, 16:27:41 UTC |
| 67656f5 | Gregory Malecha | 27 March 2014, 10:11:11 UTC | functions to well-founded spaces are well-founded. | 27 March 2014, 10:11:11 UTC |
| bfa37d2 | Gregory Malecha | 27 March 2014, 10:10:44 UTC | a setoid version of the fixpoint equation. | 27 March 2014, 10:10:44 UTC |
| d29142d | Gregory Malecha | 23 March 2014, 07:37:38 UTC | remove need for decidable equality. | 23 March 2014, 07:37:38 UTC |
