| de2fe65 | Robbert Krebbers | 08 March 2018, 21:30:34 UTC | Get rid of `'` to provide compatibility with https://github.com/coq/coq/pull/6155 This change is backwards compatible. | 08 March 2018, 21:30:34 UTC |
| 271b57d | Bas Spitters | 24 February 2018, 14:37:51 UTC | Merge pull request #49 from jashug/deprecate-implicit-arguments Change Implicit Arguments to Arguments | 24 February 2018, 14:37:51 UTC |
| 4dd044e | Jasper Hugunin | 24 February 2018, 02:01:17 UTC | Change Implicit Arguments to Arguments in CoRN | 24 February 2018, 02:01:17 UTC |
| 2010226 | Bas Spitters | 08 January 2018, 16:56:22 UTC | Merge pull request #48 from vblot/master Removed the ssreflect dependency and fixed some "Admitted" | 08 January 2018, 16:56:22 UTC |
| 5521ddd | Valentin Blot | 08 January 2018, 15:34:12 UTC | Removed the ssreflect dependency and fixed some "Admitted" | 08 January 2018, 15:39:24 UTC |
| 2309873 | Bas Spitters | 13 December 2017, 14:47:02 UTC | Merge pull request #47 from vblot/master updated SConstruct for the new version of Liouville | 13 December 2017, 14:47:02 UTC |
| de01397 | Valentin Blot | 13 December 2017, 13:39:08 UTC | updated SConstruct for the new version of Liouville | 13 December 2017, 13:39:08 UTC |
| 9478057 | Bas Spitters | 13 December 2017, 11:46:54 UTC | Merge pull request #46 from vblot/master Updated proof of Liouville's theorem | 13 December 2017, 11:46:54 UTC |
| b42486f | Valentin Blot | 12 December 2017, 21:52:52 UTC | Updated proof of Liouville's theorem | 12 December 2017, 21:52:52 UTC |
| ebe396a | Bas Spitters | 07 November 2017, 11:28:53 UTC | Merge pull request #45 from maximedenes/remove-obsolete-locality Fix obsolete vernacular syntax for locality. | 07 November 2017, 11:28:53 UTC |
| a8aefaa | Maxime Dénès | 06 November 2017, 14:09:35 UTC | Fix obsolete vernacular syntax for locality. It was emitting a deprecation warning and will soon be removed from Coq. | 07 November 2017, 09:07:03 UTC |
| 5acc6f8 | Bas Spitters | 07 November 2017, 08:52:37 UTC | Fixing Travis | 07 November 2017, 08:52:37 UTC |
| c719fad | Bas Spitters | 06 November 2017, 15:23:07 UTC | Merge pull request #44 from Zimmi48/travis Travis | 06 November 2017, 15:23:07 UTC |
| 6f11123 | Théo Zimmermann | 27 October 2017, 20:33:32 UTC | [travis] Install coq-bignums explicitly since it's a dependency. | 27 October 2017, 20:33:32 UTC |
| d67dd66 | Langston Barrett | 15 November 2016, 21:58:59 UTC | travis.yml: init make -> scons | 27 October 2017, 20:32:07 UTC |
| 7f2aab9 | Bas Spitters | 27 October 2017, 20:19:50 UTC | Merge pull request #43 from c-corn/v8.6 V8.6 | 27 October 2017, 20:19:50 UTC |
| f895f2e | Bas Spitters | 27 October 2017, 16:09:55 UTC | Update README.md | 27 October 2017, 16:09:55 UTC |
| 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 |
| bb962a0 | Matej Kosik | 17 November 2016, 12:02:02 UTC | Merge remote-tracking branch 'upstream/master' | 17 November 2016, 12:02:02 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 |
| 43c4a8e | Matej Kosik | 26 August 2016, 02:41:26 UTC | merging "v8.5" branch to "master" | 26 August 2016, 02:41:26 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 |
| 8a75145 | Bas Spitters | 08 June 2016, 10:40:20 UTC | Merge pull request #28 from coq-contribs/master adding "Make" and "Makefile" | 08 June 2016, 10:40:20 UTC |
| cd9c07a | Bas Spitters | 08 June 2016, 10:21:15 UTC | Revert "adding makefile for the benefit of contribs" This reverts commit 0ce8b11888b035feb99667cc4cd090d0f1245fae. | 08 June 2016, 10:21:15 UTC |
| 0ce8b11 | Bas Spitters | 07 June 2016, 18:06:20 UTC | adding makefile for the benefit of contribs | 07 June 2016, 18:06:20 UTC |
| fab26c9 | Matej Kosik | 06 June 2016, 15:12:34 UTC | adding "Make" and "Makefile" | 06 June 2016, 15:12:34 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 |
| efe4a33 | Bas Spitters | 31 May 2016, 08:59:24 UTC | Update README.md | 31 May 2016, 08:59:24 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 |
| 0502406 | Bas Spitters | 20 May 2016, 09:32:27 UTC | Merge pull request #26 from matej-kosik/master Fixing compilaton wrt. Coq 8.5 (d2f9a45) | 20 May 2016, 09:32:27 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 |
