551232c | Pierre-Yves Strub | 17 March 2017, 13:09:42 UTC | partition_big: generalize types | 17 March 2017, 13:09:52 UTC |
2a46a2e | Benjamin Gregoire | 17 March 2017, 11:38:15 UTC | Fix printing of random assignment | 17 March 2017, 12:50:16 UTC |
0b0bfec | Pierre-Yves Strub | 16 March 2017, 08:58:44 UTC | [list]: zip/unzip + facts | 16 March 2017, 08:58:44 UTC |
0f68ed7 | Pierre-Yves Strub | 15 March 2017, 13:41:10 UTC | Travis: test all branches marked for future integration | 15 March 2017, 13:41:10 UTC |
807b27e | Pierre-Yves Strub | 05 March 2017, 23:30:36 UTC | README | 05 March 2017, 23:30:36 UTC |
f85539c | Pierre-Yves Strub | 04 March 2017, 22:11:04 UTC | docker (nits) | 04 March 2017, 22:11:04 UTC |
572f035 | Pierre-Yves Strub | 04 March 2017, 21:08:33 UTC | nits in docker (aprhl) | 04 March 2017, 21:08:33 UTC |
ccea93c | Pierre-Yves Strub | 04 March 2017, 20:38:03 UTC | nits in docker | 04 March 2017, 20:38:12 UTC |
fd2fc2b | Pierre-Yves Strub | 04 March 2017, 09:35:08 UTC | Add support for system level conf. file Format: ini file. Sections: [general]. Options: - why3conf (string) : Why3 configuration file - provers (string list) : -P option (list of used provers) - idirs (string list) : -I option - rdirs (string list) : -R option - no-evict (string list) : -no-evict option INI file location: EasyCrypt lib. directory /etc/easycrypt.ini | 04 March 2017, 09:35:15 UTC |
4afed9d | Pierre-Yves Strub | 04 March 2017, 08:37:24 UTC | remove code dedicated to local toolchain | 04 March 2017, 08:38:49 UTC |
d633c86 | Pierre-Yves Strub | 04 March 2017, 08:27:26 UTC | update files headers (libraries) (copyright) | 04 March 2017, 08:27:26 UTC |
cd4a4d0 | Pierre-Yves Strub | 04 March 2017, 08:26:41 UTC | update files headers (copyright) | 04 March 2017, 08:26:41 UTC |
42ecbc7 | Pierre-Yves Strub | 04 March 2017, 08:26:04 UTC | Fix compilation issues | 04 March 2017, 08:26:04 UTC |
7519681 | Pierre-Yves Strub | 04 March 2017, 08:23:12 UTC | update copyright meta-data (bis) | 04 March 2017, 08:23:12 UTC |
532fd5d | Pierre-Yves Strub | 04 March 2017, 08:19:21 UTC | update copyright meta-data | 04 March 2017, 08:19:21 UTC |
249f7c1 | Pierre-Yves Strub | 02 March 2017, 09:55:54 UTC | README (opam pin) | 02 March 2017, 09:55:54 UTC |
2ebb404 | Pierre-Yves Strub | 02 March 2017, 09:55:36 UTC | [docker]: generic test box | 02 March 2017, 09:55:36 UTC |
a16c59a | Pierre-Yves Strub | 01 March 2017, 22:19:33 UTC | [README]: installing ec-branches via opam | 01 March 2017, 22:19:33 UTC |
8b2bf22 | Pierre-Yves Strub | 01 March 2017, 22:07:07 UTC | Nits on docker boxes | 01 March 2017, 22:07:07 UTC |
624a583 | Pierre-Yves Strub | 01 March 2017, 14:34:59 UTC | docker box for CI (tests) | 01 March 2017, 14:34:59 UTC |
dc91673 | Pierre-Yves Strub | 01 March 2017, 12:25:26 UTC | testting -> testing | 01 March 2017, 12:25:26 UTC |
a7c115c | Pierre-Yves Strub | 01 March 2017, 12:21:50 UTC | [make install] installs the runtest binary | 01 March 2017, 12:21:50 UTC |
bd3b7b0 | Pierre-Yves Strub | 01 March 2017, 12:21:34 UTC | Use the correct env. when printing synced prhl goals | 01 March 2017, 12:21:34 UTC |
da54edb | Pierre-Yves Strub | 01 March 2017, 11:04:22 UTC | [pprint]: when checking that 2 programs are in sync, use alpha-eq without path norm'ion | 01 March 2017, 11:04:22 UTC |
d92f237 | Pierre-Yves Strub | 01 March 2017, 10:59:06 UTC | API: access to alpha-conversion without path norm'ion | 01 March 2017, 10:59:06 UTC |
3e41975 | Pierre-Yves Strub | 01 March 2017, 10:03:32 UTC | Do not try to install non-existent PG files | 01 March 2017, 10:03:32 UTC |
df7ff31 | Pierre-Yves Strub | 01 March 2017, 09:45:31 UTC | Fix english | 01 March 2017, 09:45:31 UTC |
2950852 | Pierre-Yves Strub | 01 March 2017, 09:44:45 UTC | [pprint]: in prhl, when program as sync'ed, only display one | 01 March 2017, 09:44:45 UTC |
8f58725 | Pierre-Yves Strub | 27 February 2017, 13:18:47 UTC | README (travis status) | 27 February 2017, 13:18:47 UTC |
372fed8 | Pierre-Yves Strub | 27 February 2017, 13:14:53 UTC | Docker boxes | 27 February 2017, 13:14:53 UTC |
bec3930 | Pierre-Yves Strub | 27 February 2017, 12:56:22 UTC | Fix Travis syntax | 27 February 2017, 12:56:22 UTC |
4787ab0 | Pierre-Yves Strub | 27 February 2017, 10:44:39 UTC | Add support for travis CI. | 27 February 2017, 12:49:52 UTC |
e055841 | Pierre-Yves Strub | 27 February 2017, 10:40:22 UTC | README | 27 February 2017, 10:40:22 UTC |
ef13e8d | Pierre-Yves Strub | 23 February 2017, 08:43:14 UTC | FIx MANIFEST | 23 February 2017, 08:43:14 UTC |
2d4a41e | Pierre-Yves Strub | 21 February 2017, 22:34:38 UTC | remove emacs-based packaging script Again, docker is the way to go. | 21 February 2017, 22:34:45 UTC |
57ad58b | Pierre-Yves Strub | 21 February 2017, 22:30:40 UTC | removing local toolchain+PG, removing vagrant - opam is the way to go for getting EasyCrypt - EasyCrypt mode for PG has been integrated upstream - Vagrant is a nightmare (docker is the way to go) | 21 February 2017, 22:30:55 UTC |
263740c | François Dupressoir | 19 December 2016, 22:28:21 UTC | 'Fixing' BR93. | 19 December 2016, 22:28:21 UTC |
8acf8d0 | Benjamin Gregoire | 13 December 2016, 10:22:12 UTC | add ring on boolean in StdRing. | 13 December 2016, 10:22:45 UTC |
f993902 | Pierre-Yves Strub | 10 December 2016, 09:56:56 UTC | extra corollary in bigops | 10 December 2016, 09:56:56 UTC |
3425756 | Pierre-Yves Strub | 15 November 2016, 20:54:16 UTC | fix conversion check of expressions (missing quantif) | 15 November 2016, 20:54:22 UTC |
6700014 | Pierre-Yves Strub | 28 October 2016, 15:00:56 UTC | better use deprecated functions than non existing ones | 28 October 2016, 15:01:08 UTC |
2c150a9 | Pierre-Yves Strub | 26 October 2016, 13:57:59 UTC | kill warnings | 26 October 2016, 13:57:59 UTC |
eae4110 | Pierre-Yves Strub | 14 September 2016, 11:29:29 UTC | Makefile | 14 September 2016, 11:29:29 UTC |
495667a | Pierre-Yves Strub | 07 September 2016, 10:14:18 UTC | In `t_crush`, only substitute eqs. in variables local to the eqs. I.e., in eqs. that have been introduced after the last `split` or in all eqs. if no `split` have ocurred. [fix #17339] | 07 September 2016, 10:14:18 UTC |
5b35f66 | Pierre-Yves Strub | 07 September 2016, 10:13:01 UTC | t_subst: allow to do the substitution only in targeted hyps. The new parameter is `?tg` and gives the set of hypotheses identifiers in which the substitution can occur. If `tg` is `None`, the previous behaviour is applied --- i.e. try the substitution in all local hypotheses. | 07 September 2016, 10:13:01 UTC |
c2940eb | Pierre-Yves Strub | 07 September 2016, 10:10:42 UTC | New printer for `LDecl.hyps`. | 07 September 2016, 10:10:42 UTC |
0c51d1f | Pierre-Yves Strub | 31 August 2016, 19:10:48 UTC | Issue a warning when an unknown `pragma` is issued. The behaviour for options (i.e. for `pragma +opt` / `pragma -opt`) is kept. [close #17338] | 31 August 2016, 19:10:48 UTC |
12ed9d6 | Pierre-Yves Strub | 29 August 2016, 10:58:47 UTC | Nits in `zipper_of_cpos` (catch the right exception) | 29 August 2016, 10:58:47 UTC |
6a1a2b5 | Pierre-Yves Strub | 29 August 2016, 10:56:37 UTC | New variant of `inline`: `inline side? codepos`. Inline the procedure call located at position `codepos`. [close #17336] | 29 August 2016, 10:56:37 UTC |
3d8e4b7 | Pierre-Yves Strub | 29 August 2016, 10:25:23 UTC | Add missing cases for inline (phoare / byname) | 29 August 2016, 10:25:23 UTC |
455162b | Pierre-Yves Strub | 27 August 2016, 07:11:21 UTC | Add a pragma for interverting `/=` && `/~=` (and all their variants) The pragma is `redlogic` (i.e. logical reduction in `/=`). It is set by default. [close #17333] | 27 August 2016, 07:12:22 UTC |
d273f1b | Benjamin Gregoire | 24 August 2016, 16:28:20 UTC | add clone ComRing in BitWord | 24 August 2016, 16:28:20 UTC |
9a4f6f0 | Benjamin Gregoire | 24 August 2016, 14:58:28 UTC | add useful lemma | 24 August 2016, 14:58:28 UTC |
44c769a | Pierre-Yves Strub | 19 August 2016, 11:22:30 UTC | Syntax change: arguments of `exists` are now space separated [close #17331] | 19 August 2016, 11:22:30 UTC |
83167f7 | Pierre-Yves Strub | 19 August 2016, 10:36:02 UTC | Fix internal view's proof-term construction. [fix #17330] | 19 August 2016, 10:36:29 UTC |
d7bb00b | François Dupressoir | 11 August 2016, 16:08:59 UTC | Morefiddling with smt. | 11 August 2016, 16:08:59 UTC |
ee33eba | François Dupressoir | 11 August 2016, 12:39:35 UTC | smt all -> smt in AWord. | 11 August 2016, 12:39:35 UTC |
4f9d39d | François Dupressoir | 11 August 2016, 12:38:05 UTC | Stabilize smt in StdRing. | 11 August 2016, 12:38:05 UTC |
59c8860 | Pierre-Yves Strub | 11 August 2016, 01:53:00 UTC | Do not use hash-cons based ordering in places where a stable order in needed. Hash-cons based ordering is not stable from run to run. This commit adds a set a "natural" orderings for paths & related structure and use them in place where a stable ordering is needed. This might affect existing proofs that were, by chance, perfectly working. [fix #17329] | 11 August 2016, 02:10:53 UTC |
c4a059e | Pierre-Yves Strub | 09 August 2016, 20:52:30 UTC | New variants of i.p. `<*>` The variant `<<*>` gives priority to right-to-left substitutions, whereas the variant `<*>>` gives priority to left-to-right substitutions. [closes #17327] | 09 August 2016, 20:52:30 UTC |
8feea6f | Pierre-Yves Strub | 09 August 2016, 11:11:08 UTC | i-p `+` do not reorder goals anymore when separated by non-intro i-p. [fix #17326] | 09 August 2016, 11:11:08 UTC |
80d3044 | Pierre-Yves Strub | 08 August 2016, 13:54:01 UTC | i-p |> do not unfold anymore conclusion when applying `split` [fix #17324] | 08 August 2016, 13:54:10 UTC |
a885d8c | Pierre-Yves Strub | 07 August 2016, 21:16:03 UTC | In `crush`: do not clear substituted variables. They may still be needed by the upper layer. [fix #17323] | 07 August 2016, 21:16:03 UTC |
b0f6ae6 | Pierre-Yves Strub | 06 August 2016, 15:21:27 UTC | In subst: add support for inductive predicates. [fix #17320] | 06 August 2016, 15:21:27 UTC |
b2d38f8 | Pierre-Yves Strub | 06 August 2016, 14:10:22 UTC | In parser: `case` options are not before the colon, not after [fix #17321] | 06 August 2016, 14:10:28 UTC |
30570db | Pierre-Yves Strub | 06 August 2016, 14:05:43 UTC | In parser, do not shuffle proofs/renaming of a clone [fix #17318] | 06 August 2016, 14:05:49 UTC |
ac945f3 | Pierre-Yves Strub | 06 August 2016, 14:05:01 UTC | fix scripts w.r.t new auto DB | 06 August 2016, 14:05:01 UTC |
f6b75ac | Pierre-Yves Strub | 15 July 2016, 15:55:21 UTC | push missing files | 15 July 2016, 15:55:21 UTC |
1188240 | Benjamin Gregoire | 15 July 2016, 15:19:25 UTC | fix simplification of know real expression. | 15 July 2016, 15:19:37 UTC |
8a723c3 | Pierre-Yves Strub | 15 July 2016, 15:04:26 UTC | fix namings | 15 July 2016, 15:04:37 UTC |
293e676 | Pierre-Yves Strub | 15 July 2016, 15:00:52 UTC | some facts on ln | 15 July 2016, 15:01:01 UTC |
920939f | Pierre-Yves Strub | 15 July 2016, 14:50:24 UTC | analysis: some facts on convexity | 15 July 2016, 14:50:24 UTC |
fd59217 | Pierre-Yves Strub | 15 July 2016, 10:28:16 UTC | axiomatized bounds for ln | 15 July 2016, 10:28:29 UTC |
2e8bc62 | Pierre-Yves Strub | 15 July 2016, 10:11:10 UTC | add real square root | 15 July 2016, 10:11:10 UTC |
9a21032 | Pierre-Yves Strub | 15 July 2016, 08:23:33 UTC | async while: fix bugs regarding fresh variables | 15 July 2016, 08:26:46 UTC |
4bc331a | Pierre-Yves Strub | 15 July 2016, 07:34:43 UTC | tremendeous hacks for fixing subst. of locals | 15 July 2016, 08:26:39 UTC |
f7b4f66 | Benjamin Gregoire | 14 July 2016, 20:50:14 UTC | improve usability of async while. | 15 July 2016, 08:26:01 UTC |
c17c154 | Pierre-Yves Strub | 14 July 2016, 14:20:31 UTC | async-while prototype implementation (to be tested) | 14 July 2016, 14:20:31 UTC |
234f832 | Pierre-Yves Strub | 14 July 2016, 09:28:15 UTC | do not use Map.translate on non monotonous funs | 14 July 2016, 09:30:27 UTC |
22d52f3 | Pierre-Yves Strub | 07 July 2016, 10:26:54 UTC | Work around #17319 [references #17319] | 07 July 2016, 10:26:54 UTC |
ec6fca2 | Pierre-Yves Strub | 13 June 2016, 15:36:23 UTC | fix compilation on ocaml 4.03.0 | 13 June 2016, 15:36:32 UTC |
377a2cd | François Dupressoir | 31 May 2016, 13:25:57 UTC | NewFMap: avoid using finite sets when predicates work (eq_except). | 31 May 2016, 13:25:57 UTC |
3c30914 | François Dupressoir | 31 May 2016, 11:56:23 UTC | Stablizing an smt call in NewFMap. | 31 May 2016, 11:56:23 UTC |
c9a0683 | François Dupressoir | 19 May 2016, 10:03:13 UTC | Everything (in theories) is NewFMap. | 19 May 2016, 10:03:39 UTC |
f9d70ed | Pierre-Yves Strub | 18 May 2016, 16:09:18 UTC | balancing .dir-locals | 18 May 2016, 16:09:18 UTC |
4be663f | Pierre-Yves Strub | 17 May 2016, 16:00:05 UTC | README.md | 17 May 2016, 16:00:05 UTC |
fd4bf22 | Pierre-Yves Strub | 07 May 2016, 09:41:02 UTC | Nits. | 07 May 2016, 09:41:02 UTC |
fcf86c2 | Pierre-Yves Strub | 06 May 2016, 19:59:40 UTC | List masking. | 06 May 2016, 19:59:40 UTC |
407be6f | Pierre-Yves Strub | 06 May 2016, 14:34:18 UTC | Killing a bunch of admits in intdiv + defining ediv. | 06 May 2016, 14:34:18 UTC |
3dedf33 | Pierre-Yves Strub | 06 May 2016, 09:43:25 UTC | Don't use the currently printed abbrev. when printing its body. [fix #17135] | 06 May 2016, 09:44:11 UTC |
c8fbd0c | François Dupressoir | 06 May 2016, 08:49:44 UTC | Argmin is now a real argmin. | 06 May 2016, 08:49:44 UTC |
ff23f9a | François Dupressoir | 06 May 2016, 08:39:52 UTC | argmin: remove existentials in premises. | 06 May 2016, 08:39:52 UTC |
22578b4 | Pierre-Yves Strub | 06 May 2016, 07:38:09 UTC | `argmin` operator `argmin p` returns the smaller natural `i` s.t. `p i` or 0 if not such witness exists. | 06 May 2016, 07:38:09 UTC |
fa61550 | Pierre-Yves Strub | 05 May 2016, 19:31:40 UTC | Add negative filters for `clone ... proof * [...]` Filters now have the following syntax: `[-?tag ... -?tag]` Negative tags are of the form `-tag`. Other ones are named positive. An axiom is selected by a filter if: - none of its tags are rejected by a negative filters - one of its tags is accepted by a positive filter or no positive filters exists | 05 May 2016, 19:31:40 UTC |
6c9dfe5 | Pierre-Yves Strub | 05 May 2016, 09:28:49 UTC | Properly equip zmod with a ring structure. The inverse is currently not linked to gcd. | 05 May 2016, 09:29:36 UTC |
bf94ca4 | François Dupressoir | 04 May 2016, 11:21:37 UTC | Moving Word away from Arrays. Updating MEE functional spec accordingly. | 04 May 2016, 11:21:45 UTC |
0670411 | François Dupressoir | 04 May 2016, 11:19:46 UTC | Stabilize smt in MEE instantiation. | 04 May 2016, 11:19:46 UTC |
ccd68ba | Pierre-Yves Strub | 30 April 2016, 13:47:02 UTC | In `clone`: when renaming, don't forget to prepend sub-theorie path as a prefix. [fix #17312] | 30 April 2016, 13:47:02 UTC |
aa6ee8e | Pierre-Yves Strub | 30 April 2016, 11:30:50 UTC | Homogenise module & module type parameters syntax. [fix #17314] | 30 April 2016, 11:30:50 UTC |
6bd35fb | Pierre-Yves Strub | 30 April 2016, 10:53:33 UTC | In mod-typing: clean-up dead code, remove internal exn., fix various bugs. [fix #17313] | 30 April 2016, 10:53:33 UTC |