https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
2dbec85 Proof refactoring in List. 18 November 2015, 16:38:57 UTC
9f8c7a1 Nits in List. 18 November 2015, 15:44:36 UTC
491a6f4 sort the result of search, most relevant clause at the end. 18 November 2015, 14:42:00 UTC
b1c3bba improve theory Indepi. weaken hypothesis 18 November 2015, 14:38:30 UTC
7e470e4 Admit some properties about allpairs. 18 November 2015, 13:29:24 UTC
b7368cc Fix extra args. 18 November 2015, 12:59:29 UTC
63274eb Bits in bigops + big_allpairs. 18 November 2015, 12:36:39 UTC
aa567fe Nits on allpairs. 18 November 2015, 12:36:38 UTC
dafd55b Tuple: nits + some combinatorial results. 18 November 2015, 11:46:59 UTC
6799d54 List: allpairs def. + spec. (= cross-product \o map) 18 November 2015, 11:46:56 UTC
4091703 Nits in Lists (eq. spec. for cons/cat + hasPn). 18 November 2015, 11:46:55 UTC
29cf776 Nits (Int) 18 November 2015, 11:46:54 UTC
1c161d7 Kill all admits in Ring. 17 November 2015, 17:05:20 UTC
de7c237 Number is now admit free. 17 November 2015, 15:15:30 UTC
5399583 Fix a bunch of failing `smt` calls in stdlib. 17 November 2015, 14:03:01 UTC
34f672e Only catch CTRL-C for interactive terminals. 17 November 2015, 13:37:06 UTC
652c7b4 remove some debugging pragmas 17 November 2015, 13:34:20 UTC
3f710ab Improve the `channel` terminal - only update gc stats every 20 ticks - don't compute stats if nothing is going to be displayed - don't display gc stats by default (see the -gcstats option) This improves the checking time by 10 (disregarding smt). 17 November 2015, 13:28:11 UTC
d22f536 Fix stdlib w.r.t. new engine + kill admits in Number. 17 November 2015, 12:41:13 UTC
ab720d4 Improve pattern matching. 17 November 2015, 12:41:06 UTC
62dbbf7 Fixing internal mess about >/< 17 November 2015, 12:40:25 UTC
88c0b32 Remove internal references to >/>= 16 November 2015, 20:01:15 UTC
dbc52cc PG: add a command to print/check a term. Command name is coq-Print, acessible via C-c C-a C-p. 16 November 2015, 12:42:02 UTC
a800bcd Add ad-hoc (&& pruned) theory for words. This should be moved to Tuple. 16 November 2015, 12:14:01 UTC
08c3efb Pruning List.Array theory. 16 November 2015, 11:30:17 UTC
afca123 First pass in cleaning Int theory. 16 November 2015, 11:28:10 UTC
750b5fe Remove Int.ForLoop theory and related busted lemmas in Array. 16 November 2015, 10:24:28 UTC
d2119a5 Remove axioms for iter and kill all smt in IntExtra. 15 November 2015, 19:34:18 UTC
a8701e3 Fix binomial def. for degenerated cases + core ppts. 15 November 2015, 17:48:03 UTC
1d4e41e Def. of factorial + bin/multi. coefficients. 14 November 2015, 16:21:20 UTC
0a2ad19 Killed a tenth of admits in Number. 14 November 2015, 16:05:18 UTC
15686e8 `withbd` now applies to intro-patterns. 13 November 2015, 14:47:13 UTC
6f7f575 Nits on `b2r` 13 November 2015, 14:33:41 UTC
c46843b Update stdlib w.r.t. new fel. 13 November 2015, 09:47:32 UTC
93b5374 `fel` now uses bigops. 13 November 2015, 09:47:26 UTC
44e30af Move theories dedicated to tactics to their own directory. 13 November 2015, 09:46:47 UTC
d04384d Nits (refactoring) 13 November 2015, 09:46:45 UTC
9dba682 Remove staled & unused library (Multiset) 12 November 2015, 22:34:58 UTC
96d17ef Alias Distr/NewDistr types/ops 12 November 2015, 22:21:08 UTC
d0710e4 Kill remaining admits for real exp. 12 November 2015, 19:51:26 UTC
b23818a Nits (Fun/Ring) 12 November 2015, 19:51:24 UTC
ac99209 Add spec. for (x ^ (-n)) (Why3). 12 November 2015, 19:51:23 UTC
63c2f38 RealExp is now consistent. 12 November 2015, 18:35:34 UTC
c959c13 RealExp should now be consistent. Some axioms are still remaining. 12 November 2015, 18:25:19 UTC
34b2388 Start to fix real exp. API, adding some restrictions. 12 November 2015, 17:40:05 UTC
809f787 Remove staled comments. 12 November 2015, 15:50:53 UTC
ab30234 Start the theory of real exp. WARN: some of the axioms are plain wrong. 12 November 2015, 15:44:09 UTC
d150757 Some facts about b2i/b2r. 12 November 2015, 11:34:29 UTC
1dfe61c More b2r to the Reals theory. 12 November 2015, 11:13:59 UTC
565de6a More results in Bigalg. 12 November 2015, 11:00:32 UTC
83f7242 Clean-up lemmas and hint rewrites in alg. hierachy. 12 November 2015, 09:43:01 UTC
00dc7ab Add a new construction for clearing lemmas/hint rewrites. This command is for internal use only and will be removed in the future. 12 November 2015, 09:42:55 UTC
e318d8e Rename some theories in stdlib - Bigint.BAdd -> BIA - Bigint.BMul -> BIM - Bigreal.BAdd -> BRA - Bigreal.BMul -> BRM 11 November 2015, 16:31:48 UTC
837ac7a Add support for renaming theories in `clone` Class identifier is `theory`. 11 November 2015, 16:28:52 UTC
4b48ad2 Merge branch '1.0' into phl 11 November 2015, 15:17:19 UTC
13c3104 Fix phl stdlib w.r.t. new engine/stdlib. 11 November 2015, 15:17:12 UTC
f994bc5 Agressive imports of theories 11 November 2015, 15:10:03 UTC
976872a Change computation of implicits. Only plain variables that appear in the conclusion are marked as implicit. 11 November 2015, 15:10:03 UTC
da1840b PG: clear goal when proof is done. 11 November 2015, 14:58:03 UTC
701f875 PG: clear goal when proof is done. [fix #17266] 11 November 2015, 14:57:21 UTC
f186b7c Fix stdlib w.r.t the new implicits computation. 11 November 2015, 11:56:38 UTC
1057398 Change computation of implicits. Only plain variables that appear in the conclusion are marked as implicit. 11 November 2015, 11:56:22 UTC
8d3c12b Fix stdlib w.r.t. new syntax (pterm) 11 November 2015, 09:30:36 UTC
eb690f8 Internal: refactor implicits. Implicits can now be given by hints. 11 November 2015, 09:27:36 UTC
df3d54c Change syntax for explicit args. in pterm. The syntax is (@head args) and no more @(head args). The symbol `@` only applies to `head` and not to the sub-pterms - but can be repeated on the latter. 11 November 2015, 09:27:26 UTC
a396926 Internal: refactor implicits. Implicits can now be given by hints. 11 November 2015, 09:24:37 UTC
8dc0999 Fix stdlib w.r.t. new syntax (pterm) 10 November 2015, 20:29:02 UTC
a044d63 Change syntax for explicit args. in pterm. The syntax is (@head args) and no more @(head args). The symbol `@` only applies to `head` and not to the sub-pterms - but can be repeated on the latter. 10 November 2015, 20:28:49 UTC
4408ece runtest: check scripts collection. 10 November 2015, 16:34:59 UTC
f1a3b14 runtest: check scripts collection. 10 November 2015, 16:34:46 UTC
b24ef31 `pf_form_match` now checks that the ptenv is full instantiated. 10 November 2015, 16:12:39 UTC
b1f1acb `pf_form_match` now checks that the ptenv is full instantiated. 10 November 2015, 16:10:25 UTC
551a5d5 Fix bug in intro-pattern ordering 10 November 2015, 15:45:41 UTC
6a0ee9e remove some dup'ed lemmas 10 November 2015, 15:45:25 UTC
ebc0719 Fix bug in intro-pattern ordering 10 November 2015, 15:44:13 UTC
f3998ed Better localisation of rewrite errors. 10 November 2015, 14:22:38 UTC
6af119a Better localisation of rewrite errors. 10 November 2015, 14:22:22 UTC
f0bce89 Better localisation of intro-pattern errors. 10 November 2015, 10:07:31 UTC
8377f02 Better localisation of intro-pattern errors. 10 November 2015, 10:07:06 UTC
c4d5173 fix libraries w.r.t. new proof-engine 09 November 2015, 19:03:53 UTC
c633098 Change behaviour of `rewrite` `rewrite` now tries to unfold proof-term to find an equation to rewrite. Priority is given to `e --> true` over unfolding `e` (but the latter is tried if the former fails). 09 November 2015, 19:03:03 UTC
9a158d9 In `rewrite`, when keyed matching fails, revert to non-keyed matching. 09 November 2015, 19:01:25 UTC
6505b7e fix libraries w.r.t. new proof-engine 09 November 2015, 19:00:38 UTC
fd7673a Change behaviour of `rewrite` `rewrite` now tries to unfold proof-term to find an equation to rewrite. Priority is given to `e --> true` over unfolding `e` (but the latter is tried if the former fails). 09 November 2015, 19:00:14 UTC
8c318c9 In `rewrite`, when keyed matching fails, revert to non-keyed matching. 09 November 2015, 15:11:00 UTC
a767d8b README.md (PG) 09 November 2015, 13:13:54 UTC
8c52de6 README.md (PG) 09 November 2015, 13:13:43 UTC
0297818 Nits in Ring/Number. 08 November 2015, 19:04:22 UTC
6bc0b55 Fix a bunch of admits in Number. 08 November 2015, 17:32:11 UTC
8c38e61 More facts on num. th. 08 November 2015, 15:17:38 UTC
366f753 Fixing a bunch of admits in Number. 08 November 2015, 13:44:39 UTC
a9b6567 Fixing a bunch of admits in Number.eca. 08 November 2015, 09:54:50 UTC
7352739 More results on bigops and order. 07 November 2015, 22:13:40 UTC
749f1f7 Some results on bigops && orders. 07 November 2015, 20:36:13 UTC
157e7d0 Bigop: exchange_big. 07 November 2015, 20:07:31 UTC
f5adbec Create a dedicated Bigalg structure for number fields. 07 November 2015, 19:57:00 UTC
a911b79 Nits in Number && List. 07 November 2015, 19:31:14 UTC
361beb8 Fix a bunch of admits in Number. 06 November 2015, 15:49:17 UTC
1be9dce Fix conversion check in form. matching. 06 November 2015, 14:43:17 UTC
e9c5843 Start cleanup of Int/Ring, fix a bunch of admits in Number. 06 November 2015, 14:40:26 UTC
back to top