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