| af4b86e | Théo Zimmermann | 07 September 2021, 14:21:48 UTC | Merge pull request #161 from Zimmi48/update-ci-8.13 Update meta.yml and CI to test Coq 8.13. | 07 September 2021, 14:21:48 UTC |
| a8eb1a9 | Théo Zimmermann | 07 September 2021, 13:51:09 UTC | Update meta.yml and CI to test Coq 8.13. | 07 September 2021, 13:51:09 UTC |
| c366d3f | Bas Spitters | 09 April 2021, 20:18:09 UTC | Merge pull request #159 from mrhaandi/mod-uniform Future proof Zlcm.v and ZMod.v for | 09 April 2021, 20:18:09 UTC |
| 5fbc305 | Andrej Dudenhefner | 09 April 2021, 17:45:16 UTC | Future proof Zlcm.v and ZMod.v for https://github.com/coq/coq/pull/14086 | 09 April 2021, 17:45:16 UTC |
| b1add83 | Pierre Roux | 02 April 2021, 09:41:44 UTC | Merge pull request #158 from proux01/coq-14041 Adapt to coq/coq#14041 | 02 April 2021, 09:41:44 UTC |
| 1df0252 | Pierre Roux | 01 April 2021, 20:11:29 UTC | Adapt to coq/coq#12329 | 02 April 2021, 08:20:28 UTC |
| 155d3f3 | Pierre Roux | 01 April 2021, 10:38:40 UTC | Add a _CoqProject to ease edition | 01 April 2021, 20:15:24 UTC |
| e3f5e33 | Vincent Semeria | 26 March 2021, 10:30:11 UTC | Merge pull request #157 from coq-community/InductiveStreams Compute arctan with inductive streams | 26 March 2021, 10:30:11 UTC |
| edbde4c | Vincent Semeria | 21 March 2021, 19:19:52 UTC | Compute arctan with inductive streams | 26 March 2021, 10:04:28 UTC |
| 2778b9c | Théo Zimmermann | 15 March 2021, 09:24:50 UTC | Merge pull request #156 from Zimmi48/remove-Omega Stop requiring the Omega module. | 15 March 2021, 09:24:50 UTC |
| 3b1653d | Théo Zimmermann | 14 March 2021, 21:50:44 UTC | Stop requiring the Omega module. | 14 March 2021, 21:50:44 UTC |
| 33f0eff | Théo Zimmermann | 13 March 2021, 17:22:37 UTC | Merge pull request #155 from Zimmi48/remove-omega Remove last calls to omega. | 13 March 2021, 17:22:37 UTC |
| 5ea5f4f | Théo Zimmermann | 13 March 2021, 14:01:15 UTC | Remove last calls to omega. | 13 March 2021, 14:01:15 UTC |
| 70718b1 | Théo Zimmermann | 13 March 2021, 13:30:26 UTC | Merge pull request #154 from Zimmi48/less-omega Remove many calls to omega. | 13 March 2021, 13:30:26 UTC |
| 9bf0cf9 | Théo Zimmermann | 12 March 2021, 23:00:15 UTC | Remove many calls to omega. | 12 March 2021, 23:03:11 UTC |
| dbfa978 | Gaëtan Gilbert | 04 March 2021, 00:09:46 UTC | Merge pull request #153 from SkySkimmer/fix-ssr-setoidrw-in-hyp Don't rely on setoid rewrite forgetting arrow binder names (coq/coq#13882) | 04 March 2021, 00:09:46 UTC |
| 55721da | Gaëtan Gilbert | 02 March 2021, 11:24:28 UTC | Don't rely on setoid rewrite forgetting arrow binder names (coq/coq#13882) | 02 March 2021, 11:24:28 UTC |
| 90d0cb1 | Vincent Semeria | 21 February 2021, 20:39:43 UTC | Merge pull request #152 from coq-community/InductiveStreams Compute sine with inductive streams | 21 February 2021, 20:39:43 UTC |
| ecf2165 | Vincent Semeria | 06 December 2020, 19:31:11 UTC | Compute sine with inductive streams | 21 February 2021, 20:07:10 UTC |
| df47fd8 | Pierre-Marie Pédrot | 22 January 2021, 18:42:09 UTC | Merge pull request #151 from Zimmi48/remove-double-induction Simplify two proofs and stop using double induction. | 22 January 2021, 18:42:09 UTC |
| c2633dd | Théo Zimmermann | 21 January 2021, 08:51:57 UTC | Simplify two proofs and stop using double induction. | 21 January 2021, 13:21:17 UTC |
| 3bb2167 | Vincent Semeria | 09 January 2021, 15:30:29 UTC | Merge pull request #150 from coq-community/FixExamples Fix examples | 09 January 2021, 15:30:29 UTC |
| 4342122 | Vincent Semeria | 09 January 2021, 14:00:05 UTC | Make examples compile again | 09 January 2021, 14:21:34 UTC |
| 78421b2 | Vincent Semeria | 06 December 2020, 14:03:55 UTC | Merge pull request #149 from coq-community/InductiveStreams Improve fuel of exponential | 06 December 2020, 14:03:55 UTC |
| e10b5a3 | Vincent Semeria | 29 November 2020, 15:02:07 UTC | Improve fuel of exponential | 06 December 2020, 12:22:56 UTC |
| 42e0283 | Théo Zimmermann | 23 November 2020, 08:55:38 UTC | Merge pull request #148 from coq-community/leave-travis Switch from Travis CI to GitHub Actions. | 23 November 2020, 08:55:38 UTC |
| 4394687 | Théo Zimmermann | 23 November 2020, 08:13:35 UTC | Switch from Travis CI to GitHub Actions. | 23 November 2020, 08:13:35 UTC |
| 643fc12 | Bas Spitters | 10 November 2020, 14:26:22 UTC | Merge pull request #147 from Zimmi48/firstorder-using Stop using deprecated firstorder using syntax. | 10 November 2020, 14:26:22 UTC |
| ace2a9e | Théo Zimmermann | 10 November 2020, 14:03:07 UTC | Update .travis.yml to latest template to fix the use of the binary cache. | 10 November 2020, 14:03:07 UTC |
| a29cb96 | Théo Zimmermann | 10 November 2020, 13:36:58 UTC | Stop using deprecated firstorder using syntax. | 10 November 2020, 13:36:58 UTC |
| aca6a85 | Vincent Semeria | 30 October 2020, 08:40:36 UTC | Merge pull request #146 from coq-community/InductiveStreams Remove coinductive streams in exponential | 30 October 2020, 08:40:36 UTC |
| 05d4e20 | Vincent Semeria | 28 October 2020, 20:06:09 UTC | Remove coinductive streams in exponential | 29 October 2020, 20:53:34 UTC |
| a3faa8f | Vincent Semeria | 27 October 2020, 19:02:34 UTC | Merge pull request #145 from coq-community/InductiveStreams Replace coinductive streams by inductive streams | 27 October 2020, 19:02:34 UTC |
| c4c6b4e | Vincent Semeria | 08 October 2020, 17:58:11 UTC | Replace coinductive streams by inductive streams | 27 October 2020, 17:22:46 UTC |
| f0316f8 | Gaëtan Gilbert | 19 October 2020, 12:13:12 UTC | Merge pull request #144 from SkySkimmer/instance-gen Adapt to coq/coq#13188 (Default disable automatic generalization of Instance type) | 19 October 2020, 12:13:12 UTC |
| d119ab2 | Gaëtan Gilbert | 16 October 2020, 12:48:58 UTC | Adapt to coq/coq#13188 (Default disable automatic generalization of Instance type) | 16 October 2020, 12:48:58 UTC |
| 758b0a0 | Vincent Semeria | 04 October 2020, 16:25:29 UTC | Merge pull request #143 from coq-community/SparseRasters Sparse rasters | 04 October 2020, 16:25:29 UTC |
| 5e094f9 | Vincent Semeria | 02 October 2020, 17:32:15 UTC | Sparse rasters | 04 October 2020, 15:12:48 UTC |
| 52f675f | Vincent Semeria | 30 September 2020, 11:27:36 UTC | Merge pull request #142 from coq-community/FixAdmitted Replace Vector by list in rasters | 30 September 2020, 11:27:36 UTC |
| 96ead5f | Vincent Semeria | 29 September 2020, 17:45:01 UTC | Replace Vector by list in rasters | 30 September 2020, 09:55:22 UTC |
| db323b0 | Vincent Semeria | 28 September 2020, 15:45:34 UTC | Merge pull request #141 from coq-community/FixAdmitted Replace nat by positive in rasters | 28 September 2020, 15:45:34 UTC |
| ead680b | Vincent Semeria | 24 September 2020, 22:30:18 UTC | Replace nat by positive in rasters | 28 September 2020, 14:06:29 UTC |
| a5da641 | Vincent Semeria | 23 September 2020, 18:25:55 UTC | Merge pull request #140 from coq-community/FixAdmitted Fix extraction of sine and cosine | 23 September 2020, 18:25:55 UTC |
| d54e57e | Vincent Semeria | 23 September 2020, 16:21:10 UTC | Fix extraction of sine and cosine | 23 September 2020, 16:21:10 UTC |
| f841137 | Vincent Semeria | 22 September 2020, 21:00:32 UTC | Merge pull request #139 from coq-community/FixAdmitted Replace CoFixpoint by Fixpoint in compacts | 22 September 2020, 21:00:32 UTC |
| bbb6089 | Vincent Semeria | 21 September 2020, 21:45:15 UTC | Replace CoFixpoint by Fixpoint in compacts | 22 September 2020, 19:04:07 UTC |
| da14253 | Vincent Semeria | 21 September 2020, 12:59:32 UTC | Merge pull request #138 from coq-community/FixAdmitted Prove that compact approximations are correct | 21 September 2020, 12:59:32 UTC |
| ccee48e | Vincent Semeria | 20 September 2020, 18:43:17 UTC | Prove that compact approximations are correct | 21 September 2020, 11:39:47 UTC |
| 43e1af1 | Vincent Semeria | 19 September 2020, 13:48:13 UTC | Merge pull request #137 from coq-community/FixAdmitted Remove RSetoid from metric spaces | 19 September 2020, 13:48:13 UTC |
| 0924969 | Vincent Semeria | 14 September 2020, 21:53:11 UTC | Remove RSetoid from metric spaces Simplify step functions | 19 September 2020, 12:54:48 UTC |
| d428cb7 | Vincent Semeria | 14 September 2020, 20:53:25 UTC | Merge pull request #136 from coq-community/FixAdmitted Simplify almostIn | 14 September 2020, 20:53:25 UTC |
| d480122 | Vincent Semeria | 14 September 2020, 16:34:16 UTC | Simplify almostIn | 14 September 2020, 19:10:20 UTC |
| 2e022ab | Vincent Semeria | 14 September 2020, 11:13:22 UTC | Merge pull request #135 from coq-community/FixAdmitted Simplify InFinEnumC | 14 September 2020, 11:13:22 UTC |
| 662140c | Vincent Semeria | 13 September 2020, 12:02:12 UTC | Simplify InFinEnumC | 14 September 2020, 09:50:59 UTC |
| 9dd9b7a | Vincent Semeria | 13 September 2020, 09:12:56 UTC | Merge pull request #134 from coq-community/FixAdmitted Faster plot of circle | 13 September 2020, 09:12:56 UTC |
| 8fc28bb | Vincent Semeria | 12 September 2020, 12:18:24 UTC | Faster plot of circle | 12 September 2020, 21:43:30 UTC |
| 7425cf2 | Vincent Semeria | 11 September 2020, 10:01:19 UTC | Merge pull request #133 from coq-community/FixAdmitted Faster complex numbers | 11 September 2020, 10:01:19 UTC |
| d9af787 | Vincent Semeria | 10 September 2020, 18:46:28 UTC | Faster complex numbers | 11 September 2020, 08:37:14 UTC |
| abfbc44 | Vincent Semeria | 09 September 2020, 22:36:17 UTC | Merge pull request #132 from coq-community/FixAdmitted Fix plot of circle | 09 September 2020, 22:36:17 UTC |
| 2a10b44 | Vincent Semeria | 09 September 2020, 16:21:37 UTC | Fix plot of circle | 09 September 2020, 20:49:06 UTC |
| 7da9f14 | Vincent Semeria | 08 September 2020, 22:15:24 UTC | Merge pull request #131 from coq-community/FixAdmitted Fix admitted lemmas in faster reals | 08 September 2020, 22:15:24 UTC |
| 2a88ce9 | Vincent Semeria | 08 September 2020, 18:37:39 UTC | Fix admitted lemmas in faster reals | 08 September 2020, 21:02:55 UTC |
| b5d5813 | Vincent Semeria | 07 September 2020, 11:31:53 UTC | Merge pull request #130 from coq-community/FixAdmitted Fix some admitted lemmas | 07 September 2020, 11:31:53 UTC |
| a88d031 | Vincent Semeria | 06 September 2020, 16:24:44 UTC | Fix some admitted lemmas | 07 September 2020, 09:59:33 UTC |
| 4307bd5 | Vincent Semeria | 06 September 2020, 12:29:46 UTC | Merge pull request #129 from coq-community/FixDump Fix dump, a plugin that plots subsets of the plane | 06 September 2020, 12:29:46 UTC |
| 58f4acb | Vincent Semeria | 29 August 2020, 19:43:25 UTC | Fix dump, a plugin that plots subsets of the plane | 06 September 2020, 11:21:07 UTC |
| 0cf283c | Vincent Semeria | 03 September 2020, 07:38:23 UTC | Merge pull request #128 from coq-community/PlotSubsets Proof that plots of located subsets cover the subsets | 03 September 2020, 07:38:23 UTC |
| d1d5fd4 | Vincent Semeria | 02 September 2020, 21:13:28 UTC | Proof that plots of located subsets cover the subsets | 02 September 2020, 21:58:15 UTC |
| 4375ef9 | Vincent Semeria | 01 September 2020, 18:44:50 UTC | Merge pull request #127 from coq-community/PlotSubsets Plot located subsets of the plane | 01 September 2020, 18:44:50 UTC |
| d289ae2 | Vincent Semeria | 31 August 2020, 18:35:32 UTC | Plot located subsets of the plane | 01 September 2020, 15:50:58 UTC |
| 1efb9ec | Vincent Semeria | 28 August 2020, 19:34:54 UTC | Merge pull request #126 from coq-community/Markov Consequences of Markov's principle on constructive reals | 28 August 2020, 19:34:54 UTC |
| d1e79a1 | Vincent Semeria | 28 August 2020, 18:14:27 UTC | Consequences of Markov's principle on constructive reals | 28 August 2020, 18:14:27 UTC |
| 56abf50 | Vincent Semeria | 23 August 2020, 17:17:34 UTC | Merge pull request #125 from coq-community/CRSet Located subsets of metric spaces | 23 August 2020, 17:17:34 UTC |
| 267723f | Vincent Semeria | 23 August 2020, 11:25:27 UTC | Located subsets of metric spaces | 23 August 2020, 15:29:10 UTC |
| 73fb8f3 | Vincent Semeria | 21 August 2020, 18:53:34 UTC | Merge pull request #124 from coq-community/CRSet Move stability into the definition of metric spaces | 21 August 2020, 18:53:34 UTC |
| 1c4ebf7 | Vincent Semeria | 21 August 2020, 15:37:33 UTC | Move stability into the definition of metric spaces | 21 August 2020, 17:41:52 UTC |
| 4ec7fd0 | Vincent Semeria | 20 August 2020, 18:39:05 UTC | Merge pull request #122 from coq-community/CRSet Cut algebraic hierarchy from FinEnum | 20 August 2020, 18:39:05 UTC |
| 9c6253b | Vincent Semeria | 19 August 2020, 16:43:08 UTC | Cut algebraic hierarchy from FinEnum | 20 August 2020, 16:17:08 UTC |
| cd30592 | Vincent Semeria | 16 August 2020, 18:44:26 UTC | Merge pull request #121 from coq-community/CRSet Faster implementation of inject_Q_AR | 16 August 2020, 18:44:26 UTC |
| 64790c0 | Vincent Semeria | 16 August 2020, 17:33:45 UTC | Faster implementation of inject_Q_AR | 16 August 2020, 17:33:51 UTC |
| b2bf909 | Bas Spitters | 16 August 2020, 12:33:09 UTC | Update README.md | 16 August 2020, 12:33:09 UTC |
| af03557 | Vincent Semeria | 16 August 2020, 11:35:03 UTC | Merge pull request #120 from coq-community/CRSet Faster implementation of ARabs | 16 August 2020, 11:35:03 UTC |
| 5db1169 | Vincent Semeria | 15 August 2020, 21:52:46 UTC | Faster implementation of ARabs | 16 August 2020, 09:35:50 UTC |
| fa0cf65 | Vincent Semeria | 08 August 2020, 09:43:29 UTC | Merge pull request #118 from coq-community/CRSet Put typeclass context in a section for ConstructiveFasterReals | 08 August 2020, 09:43:29 UTC |
| 51e7365 | Vincent Semeria | 08 August 2020, 08:34:09 UTC | Put typeclass context in a section for ConstructiveFasterReals | 08 August 2020, 08:34:09 UTC |
| 1df6ab4 | Vincent Semeria | 07 August 2020, 08:04:41 UTC | Merge pull request #117 from coq-community/CRSet Prove that faster reals implement stdlib constructive reals | 07 August 2020, 08:04:41 UTC |
| f626797 | Vincent Semeria | 05 August 2020, 22:27:11 UTC | Prove that faster reals implement stdlib constructive reals | 06 August 2020, 20:18:14 UTC |
| 99d82fa | Bas Spitters | 06 August 2020, 11:24:13 UTC | Merge pull request #98 from coq-community/spitters-patch-1 Create README.md | 06 August 2020, 11:24:13 UTC |
| 110c845 | Bas Spitters | 06 August 2020, 11:23:53 UTC | Update README.md | 06 August 2020, 11:23:53 UTC |
| 9b572b1 | Vincent Semeria | 05 August 2020, 22:21:46 UTC | Merge pull request #116 from coq-community/CRSet Cut algebraic hierarchy from ARArith | 05 August 2020, 22:21:46 UTC |
| 1807a97 | Vincent Semeria | 05 August 2020, 16:03:14 UTC | Cut algebraic hierarchy from ARArith | 05 August 2020, 21:07:13 UTC |
| 1fe6f33 | Vincent Semeria | 04 August 2020, 18:55:48 UTC | Merge pull request #115 from coq-community/CRSet Prove that fast reals are Cauchy complete | 04 August 2020, 18:55:48 UTC |
| 9af8bfc | Vincent Semeria | 04 August 2020, 17:08:53 UTC | Prove that fast reals are Cauchy complete | 04 August 2020, 17:08:53 UTC |
| 4c2a664 | Vincent Semeria | 04 August 2020, 07:41:38 UTC | Merge pull request #114 from coq-community/CRSet Put fast reals in sort Set instead of Type | 04 August 2020, 07:41:38 UTC |
| 4bc90f5 | Vincent Semeria | 01 August 2020, 21:01:51 UTC | Put fast reals in sort Set instead of Type | 03 August 2020, 21:04:10 UTC |
| 70a5d57 | Vincent Semeria | 01 August 2020, 20:25:51 UTC | Merge pull request #113 from coq-community/RelicenseConstructiveMeasureTheory Relicense constructive measure theory | 01 August 2020, 20:25:51 UTC |
| 6522103 | Vincent Semeria | 01 August 2020, 18:50:39 UTC | Change license of constructive measure theory to MIT license | 01 August 2020, 18:50:39 UTC |
| fc1ee95 | Vincent Semeria | 19 July 2020, 18:48:59 UTC | Merge pull request #112 from coq-community/RemoveGball Accelerate and simplify geometric sums | 19 July 2020, 18:48:59 UTC |
| 9f61d8a | Vincent Semeria | 19 July 2020, 16:09:19 UTC | Simplify geometric sums | 19 July 2020, 17:06:16 UTC |
| fcdc94b | Vincent Semeria | 08 July 2020, 17:03:06 UTC | Cut algebraic hierarchy from CRGeometricSum | 19 July 2020, 17:06:16 UTC |
