| d849932 | Pierre-Yves Strub | 21 November 2017, 09:10:39 UTC | Merge branch 'deploy-distr' into deploy-momemtum | 21 November 2017, 09:10:39 UTC |
| 29eb9b0 | Pierre-Yves Strub | 18 November 2017, 08:59:22 UTC | All admits killed in RealSeries. | 18 November 2017, 08:59:22 UTC |
| 36a2e6a | Pierre-Yves Strub | 18 November 2017, 04:35:53 UTC | Progress | 18 November 2017, 04:35:53 UTC |
| 418d5a8 | Pierre-Yves Strub | 17 November 2017, 08:18:01 UTC | Killing more admits on summations. | 17 November 2017, 08:18:01 UTC |
| d7ebd82 | Pierre-Yves Strub | 16 November 2017, 09:59:20 UTC | Fix. | 16 November 2017, 09:59:20 UTC |
| 9f7e093 | Pierre-Yves Strub | 16 November 2017, 09:45:18 UTC | Killing more admits on real series. | 16 November 2017, 09:45:18 UTC |
| 15714a3 | Pierre-Yves Strub | 15 November 2017, 07:00:55 UTC | Make use of wlog. | 15 November 2017, 07:00:55 UTC |
| fa71435 | Pierre-Yves Strub | 15 November 2017, 06:55:54 UTC | Merge branch '1.0' into deploy-distr | 15 November 2017, 06:55:54 UTC |
| 89618eb | Pierre-Yves Strub | 15 November 2017, 06:54:48 UTC | New tactic: wlog (without loss of generality). Syntax is: wlog: x1 ... xn / form. It transforms the goal G into: |- (forall x1 ... xn, form => G) => G |- form => G | 15 November 2017, 06:54:48 UTC |
| ed2ec75 | Pierre-Yves Strub | 14 November 2017, 15:39:00 UTC | Killing admits in theory Discrete. | 14 November 2017, 15:39:00 UTC |
| 1923b91 | François Dupressoir | 14 November 2017, 14:04:42 UTC | Minimal attempt at stabilising Hybrid | 14 November 2017, 14:04:42 UTC |
| 9bdd6dd | François Dupressoir | 14 November 2017, 13:34:09 UTC | More stabilising smt in ROM | 14 November 2017, 13:34:09 UTC |
| dc92f33 | Pierre-Yves Strub | 14 November 2017, 11:43:34 UTC | More on countability. | 14 November 2017, 11:43:34 UTC |
| 1d88781 | Pierre-Yves Strub | 14 November 2017, 11:43:18 UTC | Few facts on map && injective. | 14 November 2017, 11:43:18 UTC |
| b53682b | Pierre-Yves Strub | 14 November 2017, 07:07:53 UTC | More on proving "countability" | 14 November 2017, 07:07:53 UTC |
| 2f6312c | François Dupressoir | 13 November 2017, 17:02:56 UTC | Stabilise smt in old ROM.ec | 13 November 2017, 17:06:47 UTC |
| 42ff418 | Pierre-Yves Strub | 13 November 2017, 16:06:27 UTC | Fundamental lemma of arithmetic (1st grade version) | 13 November 2017, 16:08:27 UTC |
| 8365128 | Pierre-Yves Strub | 13 November 2017, 16:08:04 UTC | Merge branch '1.0' into deploy-distr | 13 November 2017, 16:08:04 UTC |
| b95b795 | Pierre-Yves Strub | 13 November 2017, 15:06:41 UTC | In ROM.ec, help `smt` by using `move=> />`. | 13 November 2017, 15:19:53 UTC |
| 0c14bcb | Pierre-Yves Strub | 13 November 2017, 14:46:37 UTC | More on (zmodule) exponential & ordering. | 13 November 2017, 15:19:53 UTC |
| d3dcd49 | Pierre-Yves Strub | 09 November 2017, 23:27:41 UTC | New syntaxe for `pose`. `pose` can now take arguments as in `pose f i j := i + k`. | 09 November 2017, 23:27:41 UTC |
| ae2b8b8 | Pierre-Yves Strub | 09 November 2017, 23:01:16 UTC | | 09 November 2017, 23:01:16 UTC |
| 141070d | Pierre-Yves Strub | 09 November 2017, 22:49:12 UTC | Merge branch 'deploy-distr' into deploy-momemtum | 09 November 2017, 22:49:12 UTC |
| d49ff13 | Pierre-Yves Strub | 09 November 2017, 22:48:27 UTC | Merge branch '1.0' into deploy-distr | 09 November 2017, 22:48:27 UTC |
| 8781057 | Pierre-Yves Strub | 09 November 2017, 22:48:16 UTC | library: distributions: refactoring + expectation. | 09 November 2017, 22:48:16 UTC |
| 89f2173 | Pierre-Yves Strub | 07 November 2017, 09:14:11 UTC | Strengthen reduction for le/lt (int/real) | 07 November 2017, 09:14:11 UTC |
| 77f7f1c | Pierre-Yves Strub | 06 November 2017, 10:40:24 UTC | | 06 November 2017, 10:40:24 UTC |
| 0938c59 | Pierre-Yves Strub | 06 November 2017, 07:37:58 UTC | killing admits. | 06 November 2017, 07:37:58 UTC |
| 5acfa18 | Pierre-Yves Strub | 05 November 2017, 22:47:51 UTC | Killing more admits in distr. | 05 November 2017, 22:47:51 UTC |
| 7721333 | Alley Stoughton | 05 November 2017, 08:09:52 UTC | Implemented (#2) rewrite Pr [...] for mu_ge0 and mu_le1, corresponding to lemma ge0_mu (d : 'a distr) p : 0%r <= mu d p. lemma le1_mu (d : 'a distr) p : mu d p <= 1%r. from Distr.ec | 05 November 2017, 08:09:52 UTC |
| 5534f11 | Pierre-Yves Strub | 04 November 2017, 23:04:11 UTC | distr: killing more admits | 04 November 2017, 23:04:11 UTC |
| 7f64de1 | Pierre-Yves Strub | 04 November 2017, 22:36:30 UTC | docker: add support for sphinx in the doc-box. | 04 November 2017, 22:36:30 UTC |
| c7988e8 | Pierre-Yves Strub | 04 November 2017, 22:35:35 UTC | keywords script: add support for python output. | 04 November 2017, 22:35:35 UTC |
| dff1c2a | Pierre-Yves Strub | 28 October 2017, 09:23:29 UTC | | 28 October 2017, 09:23:29 UTC |
| 1a3f9a3 | Pierre-Yves Strub | 28 October 2017, 07:52:33 UTC | | 28 October 2017, 07:52:33 UTC |
| d492fcd | Pierre-Yves Strub | 27 October 2017, 07:14:18 UTC | Libraries: distributions: killing more admits | 27 October 2017, 07:14:18 UTC |
| 65dfe3c | Pierre-Yves Strub | 27 October 2017, 07:03:50 UTC | Libraries: refactoring + killing admits. | 27 October 2017, 07:03:50 UTC |
| ab29b3b | Pierre-Yves Strub | 26 October 2017, 21:55:18 UTC | Libraries: distr: killing admits | 26 October 2017, 21:55:18 UTC |
| 3f125db | Pierre-Yves Strub | 23 October 2017, 07:51:11 UTC | Libraries: proof of the Cauchy-Schwarz inequality. The proof is done for any euclidean R-ev of finite dimension. The proof comes with a characterisation of zeros for 2nd degree real polynomials. | 23 October 2017, 07:51:11 UTC |
| 9c39dce | Pierre-Yves Strub | 23 October 2017, 07:49:57 UTC | Libraries: extra facts on iterated multiplication. | 23 October 2017, 07:49:57 UTC |
| caf9b25 | Pierre-Yves Strub | 23 October 2017, 04:32:43 UTC | Libraries: solving 2nd degree real polynomials. | 23 October 2017, 04:32:43 UTC |
| fd7a34f | Pierre-Yves Strub | 23 October 2017, 04:28:35 UTC | Libraries: link Real.(^) with generic one. | 23 October 2017, 04:28:35 UTC |
| fb22315 | Pierre-Yves Strub | 23 October 2017, 04:26:57 UTC | Libraries: extra facts on the square root. | 23 October 2017, 04:26:57 UTC |
| 280f627 | Pierre-Yves Strub | 23 October 2017, 03:51:09 UTC | Add [field] as a rewrite tactic. | 23 October 2017, 03:51:09 UTC |
| 2d97328 | Pierre-Yves Strub | 23 October 2017, 02:56:49 UTC | build script: pass ECBRANCH to docker | 23 October 2017, 02:56:49 UTC |
| c2cd3f5 | Pierre-Yves Strub | 16 October 2017, 09:59:00 UTC | inline for esp | 16 October 2017, 09:59:00 UTC |
| f0a1a24 | Pierre-Yves Strub | 13 October 2017, 10:15:22 UTC | | 13 October 2017, 10:15:22 UTC |
| 70e9662 | Pierre-Yves Strub | 13 October 2017, 09:13:08 UTC | fix trans | 13 October 2017, 09:13:08 UTC |
| 3bb8f9a | Pierre-Yves Strub | 13 October 2017, 06:39:00 UTC | momemtum case can now take the final guard as an optional arg | 13 October 2017, 06:39:00 UTC |
| 8d4306c | Pierre-Yves Strub | 12 October 2017, 13:17:39 UTC | Merge branch '1.0' into deploy-momemtum | 12 October 2017, 13:17:39 UTC |
| 3b4aeec | Pierre-Yves Strub | 12 October 2017, 13:17:20 UTC | New facts on lists | 12 October 2017, 13:17:20 UTC |
| 2d7e4ab | Pierre-Yves Strub | 12 October 2017, 12:50:10 UTC | Merge branch '1.0' into deploy-momemtum | 12 October 2017, 12:50:10 UTC |
| 8999c70 | Pierre-Yves Strub | 12 October 2017, 12:50:02 UTC | New facts on lists | 12 October 2017, 12:50:02 UTC |
| a4c030e | Pierre-Yves Strub | 12 October 2017, 11:24:42 UTC | Merge branch '1.0' into deploy-momemtum | 12 October 2017, 11:24:42 UTC |
| cfa0695 | Pierre-Yves Strub | 12 October 2017, 11:24:33 UTC | Few facts on <= and exp | 12 October 2017, 11:24:33 UTC |
| 7282778 | Pierre-Yves Strub | 12 October 2017, 11:07:41 UTC | Fixing case rule (momemtum) | 12 October 2017, 11:07:41 UTC |
| 65d7c5e | Pierre-Yves Strub | 12 October 2017, 11:01:30 UTC | Fixing case rule (momemtum) | 12 October 2017, 11:01:30 UTC |
| bf7e2da | Pierre-Yves Strub | 10 October 2017, 22:47:30 UTC | momemtum trans: do not use existentials over memories | 10 October 2017, 22:47:30 UTC |
| 75aa932 | Pierre-Yves Strub | 10 October 2017, 22:28:32 UTC | momemtum-case with conseq | 10 October 2017, 22:28:32 UTC |
| 940baad | Pierre-Yves Strub | 10 October 2017, 07:33:04 UTC | basic facts on bigo | 10 October 2017, 07:33:04 UTC |
| 6864786 | Pierre-Yves Strub | 10 October 2017, 07:05:54 UTC | Merge branch '1.0' into deploy-momemtum | 10 October 2017, 07:05:54 UTC |
| 56964f5 | Pierre-Yves Strub | 10 October 2017, 07:04:02 UTC | Update installation instructions for Windows (using opam). | 10 October 2017, 07:04:02 UTC |
| 10a2fc7 | Pierre-Yves Strub | 10 October 2017, 07:03:49 UTC | Binary packages automatisation scripts. | 10 October 2017, 07:03:49 UTC |
| 6578414 | Pierre-Yves Strub | 06 October 2017, 13:00:43 UTC | Merge branch 'deploy-bin-packages' into deploy-momemtum | 06 October 2017, 13:00:43 UTC |
| aaf1981 | Pierre-Yves Strub | 06 October 2017, 12:57:06 UTC | EspMult rule | 06 October 2017, 12:57:06 UTC |
| a066dc5 | Pierre-Yves Strub | 06 October 2017, 11:55:13 UTC | | 06 October 2017, 11:55:13 UTC |
| a2a7197 | Pierre-Yves Strub | 05 October 2017, 05:25:02 UTC | | 05 October 2017, 05:25:02 UTC |
| 8ef429c | Pierre-Yves Strub | 05 October 2017, 05:10:16 UTC | Why3.conf for win32 | 05 October 2017, 05:10:16 UTC |
| 5e53d82 | Pierre-Yves Strub | 03 October 2017, 18:46:44 UTC | Merge branch '1.0' into deploy-bin-packages | 03 October 2017, 18:46:44 UTC |
| f19df51 | Pierre-Yves Strub | 03 October 2017, 07:08:00 UTC | | 03 October 2017, 07:08:00 UTC |
| 91b30d9 | Pierre-Yves Strub | 03 October 2017, 07:06:49 UTC | | 03 October 2017, 07:06:49 UTC |
| a771cb6 | Pierre-Yves Strub | 03 October 2017, 05:51:32 UTC | Finalize trans rule | 03 October 2017, 05:51:32 UTC |
| 9db99ca | Pierre-Yves Strub | 03 October 2017, 05:33:53 UTC | Trans (placeholder for missing hyph) | 03 October 2017, 05:33:53 UTC |
| d1476c6 | Pierre-Yves Strub | 03 October 2017, 05:32:47 UTC | New implementation of trans (partial) | 03 October 2017, 05:32:47 UTC |
| 20fcbc3 | Pierre-Yves Strub | 02 October 2017, 10:58:06 UTC | Extra facts on bigo | 02 October 2017, 10:58:06 UTC |
| 89fb774 | François Dupressoir | 02 August 2017, 16:25:38 UTC | exclude examples/incomplete recursively | 28 September 2017, 11:37:51 UTC |
| 7cee24f | François Dupressoir | 02 August 2017, 16:25:11 UTC | Support recursive exclusions in test targets | 28 September 2017, 11:37:51 UTC |
| b39d7a2 | Pierre-Yves Strub | 28 September 2017, 11:28:42 UTC | Fix theories after merge with 1.0 | 28 September 2017, 11:28:42 UTC |
| 5036f20 | Pierre-Yves Strub | 27 September 2017, 13:19:43 UTC | Merge branch '1.0' into momentum | 27 September 2017, 13:19:43 UTC |
| a3730c8 | Pierre-Yves Strub | 06 September 2017, 09:00:31 UTC | Fixing packages config/scripts | 06 September 2017, 09:00:31 UTC |
| e657919 | Pierre-Yves Strub | 05 September 2017, 13:14:44 UTC | Initial app for macos | 05 September 2017, 13:14:56 UTC |
| 921d07a | Francois Dupressoir | 05 September 2017, 09:46:48 UTC | Minor fixes in README.md | 05 September 2017, 09:46:48 UTC |
| 5f98708 | Pierre-Yves Strub | 05 September 2017, 08:51:05 UTC | Installation instructions for Win32 | 05 September 2017, 08:51:05 UTC |
| 5e16079 | Pierre-Yves Strub | 05 September 2017, 08:45:18 UTC | make _tags compatible with opam/win32 | 05 September 2017, 08:45:18 UTC |
| 0ec06f1 | Pierre-Yves Strub | 04 September 2017, 14:26:21 UTC | Done with AppImage | 04 September 2017, 14:26:21 UTC |
| 8b91c12 | Pierre-Yves Strub | 04 September 2017, 11:47:04 UTC | First app-image try | 04 September 2017, 11:47:04 UTC |
| 44ae0e6 | François Dupressoir | 25 August 2017, 09:35:52 UTC | typo in error message (ecHiGoal) | 25 August 2017, 09:36:18 UTC |
| 3e7dc31 | François Dupressoir | 21 August 2017, 16:29:20 UTC | moving ahead - some admits in FEL application | 21 August 2017, 16:29:20 UTC |
| ac19323 | François Dupressoir | 11 August 2017, 16:15:49 UTC | oaep: experimenting with fel flexibility and style | 11 August 2017, 16:15:49 UTC |
| 2a78686 | François Dupressoir | 11 August 2017, 16:15:05 UTC | typos in Distr (comments) | 11 August 2017, 16:15:05 UTC |
| 379e448 | François Dupressoir | 10 August 2017, 21:33:27 UTC | oaep: some progress | 10 August 2017, 21:33:31 UTC |
| 9329d72 | François Dupressoir | 03 August 2017, 15:36:15 UTC | oaep: exploring useful intermediate lemmas | 03 August 2017, 15:36:15 UTC |
| a2de959 | François Dupressoir | 02 August 2017, 15:25:38 UTC | Cleanup in examples: deleting some, porting some. | 02 August 2017, 15:25:38 UTC |
| c589262 | François Dupressoir | 31 July 2017, 11:27:25 UTC | OAEP progress | 31 July 2017, 11:27:39 UTC |
| 68f7b62 | Benjamin Gregoire | 28 July 2017, 10:22:23 UTC | remove garbage | 28 July 2017, 10:22:23 UTC |
| d5c7c6e | Benjamin Gregoire | 28 July 2017, 09:57:53 UTC | full proof of cramer shoup :-) | 28 July 2017, 09:58:12 UTC |
| 00a61be | Benjamin Gregoire | 28 July 2017, 06:05:18 UTC | new theory allowing to switch from a sampling d to a sampling d \ X | 28 July 2017, 09:58:12 UTC |
| cbeb6f3 | Benjamin Gregoire | 28 July 2017, 06:04:26 UTC | more lemmas | 28 July 2017, 09:58:12 UTC |
| 55cc1ec | Benjamin Gregoire | 28 July 2017, 06:03:58 UTC | fix bug in typing of projection on tuple. case the tuple as type "glob M" | 28 July 2017, 09:58:12 UTC |
| 00cc7d0 | Benjamin Gregoire | 28 July 2017, 04:19:44 UTC | intermediary stuff | 28 July 2017, 09:58:12 UTC |
