| 8a64c76 | Bas Spitters | 27 October 2017, 16:07:50 UTC | Merge pull request #42 from letouzey/external-bignums corn : switch to the external Bignums library | 27 October 2017, 16:07:50 UTC |
| 9e71c60 | Pierre Letouzey | 10 June 2017, 15:29:46 UTC | corn : switch to the external Bignums library See PR#498 https://github.com/coq/coq/pull/498 In addition to this commit, you should also have fetched and compiled the new bignums packages before compiling math-classes and corn : git clone https://github.com/coq/bignums.git && cd bignums && make && make install | 10 June 2017, 15:29:46 UTC |
| 226b25a | Bas Spitters | 17 March 2017, 09:42:06 UTC | Merge pull request #41 from Zimmi48/fix-for-coq-pr-474 Thanks! fix unused variable name warnings | 17 March 2017, 09:42:06 UTC |
| 3159399 | Bas Spitters | 17 March 2017, 09:40:51 UTC | Merge pull request #40 from silene/IZR Thanks! Make proofs oblivious to the changes in the definition of IZR. | 17 March 2017, 09:40:51 UTC |
| 30065bd | Théo Zimmermann | 14 March 2017, 10:00:42 UTC | fix unused variable name warnings | 14 March 2017, 10:00:42 UTC |
| 264a317 | Guillaume Melquiond | 08 March 2017, 08:29:22 UTC | Make proofs oblivious to the changes in the definition of IZR. | 08 March 2017, 08:29:22 UTC |
| 08a831c | Matthieu Sozeau | 31 October 2016, 10:04:10 UTC | Fix for new TCS implem, silent shelved goals remained Also spotted a strange unification taking ages | 31 October 2016, 10:05:31 UTC |
| 8b298b2 | Matthieu Sozeau | 27 June 2016, 15:04:11 UTC | Temporary fix for script which revealed an error in eauto with typeclass_instances. | 27 June 2016, 15:05:13 UTC |
| 877e1be | Pierre Letouzey | 24 June 2016, 14:49:29 UTC | Makefile: no more message about a Circular Make <- Makefile.coq dependency dropped | 24 June 2016, 14:49:29 UTC |
| 06b22f0 | Matej Kosik | 06 June 2016, 15:11:43 UTC | adding "Make" and "Makefile" | 06 June 2016, 15:11:43 UTC |
| efa29a4 | Bas Spitters | 31 May 2016, 09:00:12 UTC | Update README.md | 31 May 2016, 09:00:12 UTC |
| 59f43af | Bas Spitters | 20 May 2016, 09:34:13 UTC | Merge pull request #27 from matej-kosik/trunk Fixing compilaton wrt. Coq trunk (244d7a9) | 20 May 2016, 09:34:13 UTC |
| 94d6ecb | Matej Kosik | 19 May 2016, 17:00:12 UTC | Merge branch 'master' into trunk | 19 May 2016, 17:00:12 UTC |
| 533befb | Matej Kosik | 19 May 2016, 16:59:37 UTC | Changing "configure.sh" so that it considers also the $COQBIN variable. | 19 May 2016, 16:59:37 UTC |
| 6d86f64 | Matej Kosik | 19 May 2016, 14:22:57 UTC | Fixing compilation wrt. Coq trunk | 19 May 2016, 14:22:57 UTC |
| 14bb3fa | Matej Kosik | 19 May 2016, 12:57:25 UTC | Fixing compilaton wrt. Coq 8.5 | 19 May 2016, 13:23:49 UTC |
| cc2a7e3 | Abhishek Anand (@brixpro-home) | 20 April 2016, 01:00:40 UTC | ARtrans.vo compiling in Coq 8.5, proofs containing admit need to end with Admitted (and not Qed or Defined) | 20 April 2016, 01:00:40 UTC |
| 56235c7 | Abhishek Anand | 23 March 2016, 02:57:40 UTC | crtrans.vo is compiling via scons. MathClasses was copied to /usr/local/.../coq/lib/user_contribs/ | 20 April 2016, 00:37:16 UTC |
| 55de8eb | Abhishek Anand (@brixpro-home) | 20 April 2016, 00:28:43 UTC | fully quanified imports to MathClasses. These references were added in the trunk branch, and therefore did not get fixed by Jason's fix to the master branch. | 20 April 2016, 00:28:43 UTC |
| a6c619c | Abhishek Anand (@brixpro-home) | 19 April 2016, 23:20:37 UTC | Merge branch 'cornmaster' into allfixes | 19 April 2016, 23:20:37 UTC |
| e9162ea | Robbert Krebbers | 03 March 2016, 11:11:37 UTC | Merge pull request #24 from bmsherman/imports Make import statements absolute and other small changes | 03 March 2016, 11:11:37 UTC |
| 55dc222 | Ben Sherman | 01 March 2016, 22:05:14 UTC | Comment out computation in Picard | 01 March 2016, 22:05:14 UTC |
| ed87007 | Ben Sherman | 01 March 2016, 21:38:44 UTC | Reduce [big] parameter in alternating sum length computation | 01 March 2016, 21:38:44 UTC |
| 6411967 | Ben Sherman | 01 March 2016, 20:23:18 UTC | Absolutize all [Import]s Use Jason Gross's `absolutize-imports.py` script to make all [Import] statements use absolute paths rather than just relative paths, which fixes errors for case-insensitive filesystems. See: https://gist.github.com/JasonGross/14decf638535a2447286 https://github.com/JasonGross/coq-tools | 01 March 2016, 20:23:18 UTC |
| 7bce94c | Bas Spitters | 05 December 2015, 18:49:02 UTC | Merge pull request #22 from clarus/master README in MarkDown with OPAM instructions | 05 December 2015, 18:49:02 UTC |
| 00fe2f2 | Guillaume Claret | 26 November 2015, 17:10:46 UTC | README in MarkDown with OPAM instructions | 26 November 2015, 17:10:46 UTC |
| e14d3b4 | Subramanian Mahadevan | 08 June 2015, 05:03:31 UTC | minimal patch to compile CoRN on Mac following recent patch to MathClasses for case-sensitive file systems (https://github.com/math-classes/math-classes/commit/9330ab1133da24bcd2deee9e26ae27988b13c63a); minimal patch also applies to Windows; a more comprehensive fix with complete require paths like MathClasses may be preferable | 08 June 2015, 05:03:31 UTC |
| 0e9fad5 | Bas Spitters | 29 May 2015, 10:57:09 UTC | Merge pull request #20 from spitters/master Updating README, resolving #19 | 29 May 2015, 10:57:09 UTC |
| e1f891d | Bas Spitters | 29 May 2015, 10:53:44 UTC | Updating README, resolving #19 | 29 May 2015, 10:53:44 UTC |
| f5d98c7 | Bas Spitters | 14 March 2015, 18:23:08 UTC | Merge pull request #14 from aa755/PullReq 3 lemmas. 1) intervals are convex 2) Min is contained in any interval containing the 2 args 3) same for max | 14 March 2015, 18:23:08 UTC |
| b55120c | Bas Spitters | 25 February 2015, 01:56:26 UTC | Merge pull request #5 from clarus/master Preparation for Opam | 25 February 2015, 01:56:26 UTC |
| d829dc9 | Abhishek Anand | 09 January 2015, 23:23:13 UTC | added 2 lemmas. Min and Max are contained in any interval containing the 2 arguments. | 09 January 2015, 23:23:13 UTC |
| 0146ce7 | Abhishek Anand | 09 January 2015, 20:28:21 UTC | added a simple lemma stating convexity of [interval]s | 09 January 2015, 20:28:21 UTC |
| 640b956 | Robbert Krebbers | 30 December 2014, 07:27:41 UTC | Merge pull request #13 from aa755/PullReq added the Weak_IVTQ lemma which is a stronger variant of Weak_IVT | 30 December 2014, 07:27:41 UTC |
| 294cf54 | Abhishek Anand | 30 December 2014, 00:39:06 UTC | removed some unnecessary hints and lemmas | 30 December 2014, 00:39:06 UTC |
| efb6acd | Abhishek Anand | 30 December 2014, 00:08:08 UTC | added the Weak_IVTQ lemma which is a stronger variant of CoRN.ftc.StrongIVT.Weak_IVT | 30 December 2014, 00:08:08 UTC |
| 0da96ae | Guillaume Claret | 25 September 2014, 16:22:07 UTC | The configure generate Make using find | 25 September 2014, 16:22:07 UTC |
| d89f0da | Guillaume Claret | 25 September 2014, 16:17:49 UTC | Required old file added back | 25 September 2014, 16:17:49 UTC |
| 8518e5c | Guillaume Claret | 25 September 2014, 16:16:26 UTC | SConstruct is back | 25 September 2014, 16:16:26 UTC |
| 0e342f2 | Guillaume Claret | 25 September 2014, 16:16:15 UTC | rational.ml not used anymore | 25 September 2014, 16:16:15 UTC |
| 318d7dd | Bas Spitters | 25 September 2014, 15:54:32 UTC | Remoing obsolete tactic | 25 September 2014, 15:54:32 UTC |
| 6194dda | Bas Spitters | 25 September 2014, 15:49:10 UTC | Merge branch 'trunk' of https://github.com/c-corn/corn into trunk | 25 September 2014, 15:49:10 UTC |
| 3854436 | Bas Spitters | 25 September 2014, 15:45:39 UTC | Removing unused tactics | 25 September 2014, 15:45:39 UTC |
| b5a64b7 | Guillaume Claret | 22 September 2014, 11:21:29 UTC | Some files commented out | 22 September 2014, 11:21:29 UTC |
| dca17b0 | Guillaume Claret | 22 September 2014, 00:18:34 UTC | old/ folder removed | 22 September 2014, 00:18:34 UTC |
| 437eda3 | Guillaume Claret | 22 September 2014, 00:18:13 UTC | Non-compiling files removed | 22 September 2014, 00:18:13 UTC |
| 72696f3 | Guillaume Claret | 21 September 2014, 22:03:09 UTC | Math Classes Git module removed, SCons replaced by Coq Makefile | 21 September 2014, 22:03:09 UTC |
| 036fdea | Bas Spitters | 18 September 2014, 16:31:29 UTC | Merge pull request #4 from spitters/trunk Trunk | 18 September 2014, 16:31:29 UTC |
| 82325fb | Bas Spitters | 18 September 2014, 16:22:35 UTC | update README | 18 September 2014, 16:22:35 UTC |
| cc4f9d6 | Bas Spitters | 18 September 2014, 16:20:16 UTC | Make compile with trunk | 18 September 2014, 16:20:16 UTC |
| 039830e | Bas Spitters | 02 September 2014, 18:14:10 UTC | Merge pull request #3 from spitters/trunk Trunk | 02 September 2014, 18:14:10 UTC |
| 05d24df | Bas Spitters | 02 September 2014, 17:56:47 UTC | Cleaning up | 02 September 2014, 17:56:47 UTC |
| c8c1921 | Bas Spitters | 02 September 2014, 15:53:11 UTC | Removing admit. | 02 September 2014, 15:53:11 UTC |
| d6b1a6d | Bas Spitters | 02 September 2014, 15:36:47 UTC | Removing dependency | 02 September 2014, 15:36:47 UTC |
| 86854d9 | Bas Spitters | 02 September 2014, 15:21:06 UTC | Removing some old tactics. | 02 September 2014, 15:21:06 UTC |
| 7bbcb66 | Bas Spitters | 01 September 2014, 20:13:24 UTC | updating | 01 September 2014, 20:13:24 UTC |
| c9fc701 | Bas Spitters | 01 September 2014, 14:41:21 UTC | Adding files | 01 September 2014, 14:41:21 UTC |
| 70389f3 | Bas Spitters | 01 September 2014, 14:00:25 UTC | Moving files. | 01 September 2014, 14:00:25 UTC |
| beec5f2 | Bas Spitters | 01 September 2014, 13:21:16 UTC | Adding file | 01 September 2014, 13:21:16 UTC |
| 29c650d | Bas Spitters | 01 September 2014, 06:19:37 UTC | Merge pull request #1 from aa755/master Update CSumsReals.v | 01 September 2014, 06:19:37 UTC |
| 1152118 | Abhishek Anand | 31 August 2014, 23:19:46 UTC | Update CSumsReals.v fixed a minor typo | 31 August 2014, 23:19:46 UTC |
| e1a44aa | Bas Spitters | 29 August 2014, 15:21:14 UTC | Making compile with trunk | 29 August 2014, 15:21:14 UTC |
| 184c69a | Bas Spitters | 27 August 2014, 15:52:44 UTC | In the process of making compile with trunk | 27 August 2014, 15:52:44 UTC |
| 228a059 | Bas Spitters | 26 August 2014, 10:41:11 UTC | Merge pull request #2 from spitters/trunk Trunk | 26 August 2014, 10:41:11 UTC |
| e879504 | Bas Spitters | 26 August 2014, 10:27:41 UTC | updating README | 26 August 2014, 10:27:41 UTC |
| 0849283 | Bas Spitters | 25 August 2014, 14:22:05 UTC | Adding .aux .native | 25 August 2014, 14:22:05 UTC |
| 4d76587 | Bas Spitters | 02 June 2014, 16:31:46 UTC | Removing html files here, as they are now on: https://github.com/c-corn/c-corn.github.com | 02 June 2014, 16:31:46 UTC |
| 1d0c7c0 | Bas Spitters | 23 May 2014, 12:38:19 UTC | Small changes in example | 23 May 2014, 12:38:19 UTC |
| abc1395 | Bas Spitters | 04 April 2014, 16:31:09 UTC | Updating description | 04 April 2014, 16:31:09 UTC |
| d82c441 | Bas Spitters | 03 April 2014, 14:19:42 UTC | Now works ith 8.4pl4 | 03 April 2014, 14:19:42 UTC |
| 6177545 | Bas Spitters | 03 April 2014, 12:23:36 UTC | Updating the math-classes submodule | 03 April 2014, 12:23:36 UTC |
| 27a36b2 | Bas Spitters | 01 July 2013, 09:55:04 UTC | merging | 01 July 2013, 09:55:04 UTC |
| cc2a62e | Evgeny Makarov | 10 May 2013, 09:21:52 UTC | Commented out computations that take too long in Picard.v | 10 May 2013, 09:21:52 UTC |
| 0a75d15 | Evgeny Makarov | 28 April 2013, 19:37:28 UTC | Removed all admit's. Proved that Picard iterations converge to the solution of an integral equation. | 28 April 2013, 19:37:28 UTC |
| 79c6dc6 | Evgeny Makarov | 22 April 2013, 00:36:26 UTC | Did computational experiments | 22 April 2013, 00:36:26 UTC |
| f1bd925 | Evgeny Makarov | 20 April 2013, 21:56:45 UTC | Proved lemmas needed for computational example | 20 April 2013, 21:56:45 UTC |
| 4855512 | Evgeny Makarov | 19 April 2013, 23:17:42 UTC | Proved that the integral of a sum equals the sum of integrals | 19 April 2013, 23:17:42 UTC |
| e16593e | Evgeny Makarov | 16 April 2013, 21:56:24 UTC | Made AbstractIntegration.v require SimpleIntegration.v instead of the other way around. SimpleIntegration.v defines integral for uniformly comtinuous functions; AbstractIntegration.v proves properties of integral. Also proved several lemmas about rational numbers. | 16 April 2013, 22:01:02 UTC |
| d790bbc | Evgeny Makarov | 05 April 2013, 20:05:30 UTC | Proved all lemmas outside of Picard.v | 05 April 2013, 20:05:30 UTC |
| 3799b0c | Evgeny Makarov | 02 April 2013, 18:53:31 UTC | Proved several lemmas | 02 April 2013, 18:53:31 UTC |
| 686ce02 | Evgeny Makarov | 20 March 2013, 21:03:40 UTC | Proved that unformly continuous functions are closed under addition and negation | 20 March 2013, 21:03:40 UTC |
| 0769db9 | Evgeny Makarov | 26 February 2013, 21:11:21 UTC | . | 26 February 2013, 21:11:21 UTC |
| 216d75f | Evgeny Makarov | 22 February 2013, 19:11:02 UTC | Proved some lemmas | 22 February 2013, 19:11:02 UTC |
| f3953a8 | Evgeny Makarov | 18 February 2013, 23:17:39 UTC | Proved that Picard operator has a fixpoint | 18 February 2013, 23:17:39 UTC |
| 5f01698 | Evgeny Makarov | 17 February 2013, 23:46:16 UTC | Proved that Picard operator is a contraction | 17 February 2013, 23:46:16 UTC |
| 75c5e4b | Evgeny Makarov | 16 February 2013, 16:51:06 UTC | Updated README: Coq 8.4pl1 instead of beta EvgenyMakarov in URL instead of c-corn | 16 February 2013, 16:51:06 UTC |
| bc16c56 | Evgeny Makarov | 16 February 2013, 16:37:30 UTC | Added the ode/ directory to SConstruct to be compiled | 16 February 2013, 16:37:30 UTC |
| 3b7e09b | Evgeny Makarov | 16 February 2013, 16:23:37 UTC | Merged master and UC (UniformlyContinuous) | 16 February 2013, 16:23:37 UTC |
| bbd13ac | Evgeny Makarov | 14 February 2013, 20:51:13 UTC | . | 14 February 2013, 20:51:13 UTC |
| 4f437f5 | Evgeny Makarov | 13 February 2013, 20:50:56 UTC | . | 13 February 2013, 20:50:56 UTC |
| 3dc2166 | Evgeny Makarov | 12 February 2013, 22:01:42 UTC | . | 12 February 2013, 22:01:42 UTC |
| f4a0b6b | Evgeny Makarov | 11 February 2013, 21:42:00 UTC | Made BanachFixpoint.v compile | 11 February 2013, 21:42:00 UTC |
| a34e5ea | Evgeny Makarov | 07 February 2013, 03:04:49 UTC | Moved ODE solver files to ode/ | 07 February 2013, 03:04:49 UTC |
| ef2c3c1 | Evgeny Makarov | 07 February 2013, 03:01:44 UTC | Created directory 'ode' for ODE solvers | 07 February 2013, 03:01:44 UTC |
| 2da833f | Evgeny Makarov | 07 February 2013, 01:54:26 UTC | Changed Picard iterations from Lipschitz to UniformlyContinuous. Tested iterations. | 07 February 2013, 01:54:26 UTC |
| f6aa710 | Evgeny Makarov | 05 February 2013, 17:16:51 UTC | . | 05 February 2013, 17:16:51 UTC |
| 32b8f32 | Evgeny Makarov | 04 February 2013, 23:29:24 UTC | Proved that the image of the image of the Picard operator lies in the required segment | 04 February 2013, 23:29:24 UTC |
| ce84ea6 | Evgeny Makarov | 02 February 2013, 22:25:05 UTC | Proved that the result of the Picard operators is Lipschitz | 02 February 2013, 22:25:05 UTC |
| 17b76c9 | Evgeny Makarov | 31 January 2013, 22:41:31 UTC | Proved that extension of a Lipschitz function is Lipschitz | 31 January 2013, 22:41:31 UTC |
| 2d98acb | Evgeny Makarov | 30 January 2013, 22:28:46 UTC | Proving that extend is Lipschitz | 30 January 2013, 22:28:46 UTC |
