| 729a333 | b | 07 June 2019, 12:26:49 UTC | rename contract | 07 June 2019, 12:26:49 UTC |
| 5c561bf | b | 07 June 2019, 10:49:34 UTC | return to sender | 07 June 2019, 10:50:37 UTC |
| c0b89f6 | Basile Pesin | 05 June 2019, 10:03:10 UTC | New proven smart-contract: vote.tz | 05 June 2019, 10:03:10 UTC |
| a0d465c | Basile Pesin | 29 May 2019, 09:23:15 UTC | Removed duplicate rule | 31 May 2019, 15:44:47 UTC |
| 443304c | Basile Pesin | 29 May 2019, 09:05:34 UTC | Updated michocott README | 31 May 2019, 15:44:46 UTC |
| 721313e | Basile Pesin | 29 May 2019, 09:01:49 UTC | Fixed michocott pdf generation | 31 May 2019, 15:44:16 UTC |
| 1018b2d | Raphaël Cauderlier | 31 May 2019, 11:56:31 UTC | Proofs of extensionality for sets and maps | 31 May 2019, 11:56:31 UTC |
| 877a6f2 | Basile Pesin | 27 May 2019, 13:13:29 UTC | Corrected typo | 27 May 2019, 13:13:29 UTC |
| 50b434e | Raphaël Cauderlier | 23 May 2019, 11:45:27 UTC | Add a tikz version of the Tezos logo | 23 May 2019, 11:45:27 UTC |
| 38f7ba5 | Raphaël Cauderlier | 20 May 2019, 15:40:27 UTC | [Doc] Add missing tezos logo | 20 May 2019, 15:40:27 UTC |
| 7adba0e | Raphaël Cauderlier | 20 May 2019, 15:38:19 UTC | [Doc] Update the Irif seminar slides | 20 May 2019, 15:38:19 UTC |
| f23ea6e | Raphaël Cauderlier | 18 May 2019, 14:35:01 UTC | [Doc] Add a logo for Mi-Cho-Coq | 18 May 2019, 14:35:34 UTC |
| 2a7d174 | Raphaël Cauderlier | 18 May 2019, 10:46:46 UTC | [Doc] Add a "singing battery" logo This logo is a pun in french, - "la pie qui chante" (literally "the singing magpie") is a french brand producing the Mi-Cho-Ko candies - "pile" in french means both "stack" and "battery" | 18 May 2019, 10:46:46 UTC |
| 0851734 | Raphaël Cauderlier | 17 May 2019, 22:38:03 UTC | [Doc] Slides for the seminar of the verification team of Irif | 17 May 2019, 22:39:50 UTC |
| b479da0 | Raphaël Cauderlier | 17 May 2019, 18:00:27 UTC | [Manager contract] Add the possiblity to send tokens to the contract without being the manager | 17 May 2019, 18:00:27 UTC |
| 398d4a6 | Raphaël Cauderlier | 17 May 2019, 15:22:18 UTC | New proven smart contract: manager.tz This contract can be used as a replacement of scriptless KT1s. | 17 May 2019, 15:22:18 UTC |
| 59f1f4b | Raphael Cauderlier | 05 April 2019, 08:53:13 UTC | [FIX] Makes the `address` type comparable. Contrary to what the documentation of Michelson claims, the `address` type is comparable in the OCaml implementation. This commit makes it comparable in Mi-Cho-Coq too. | 17 May 2019, 13:53:30 UTC |
| 53f7fcd | b | 18 March 2019, 09:56:01 UTC | [Michocoq] list_ -> list, option_ -> option, set_ -> set | 09 April 2019, 08:42:33 UTC |
| 65729a8 | Raphaël Cauderlier | 05 April 2019, 14:14:45 UTC | [CI] Install a recent version of `shellcheck` | 09 April 2019, 07:23:48 UTC |
| b4b5e0e | Brian Guo | 04 April 2019, 16:39:17 UTC | [fix] configure files in src subdirectories should now also work for mac | 09 April 2019, 07:23:48 UTC |
| 044efcc | Brian Guo | 05 April 2019, 20:18:13 UTC | [add] moved important tactics to util file; used tactics in multisig | 05 April 2019, 20:18:13 UTC |
| e2e399c | Raphael Cauderlier | 03 April 2019, 14:03:44 UTC | [CI] Continuous integration The CI script does the following: - lint the `configure` shell scripts using `shellcheck` - lint the file `README.org` using `org-lint` - compile the project with Coq v8.8 and Coq v8.9. | 03 April 2019, 14:03:44 UTC |
| baa2a13 | Raphael Cauderlier | 03 April 2019, 14:01:28 UTC | [multisig] Replace `injection; discriminate` by `discriminate`. Some versions of Coq fail at useless calls to `injection`. | 03 April 2019, 14:01:28 UTC |
| 9019629 | Raphael Cauderlier | 03 April 2019, 14:00:31 UTC | [build] By default, do not build the documentation | 03 April 2019, 14:00:31 UTC |
| 029eead | Raphael Cauderlier | 23 March 2019, 05:57:26 UTC | [Build] Drop support for Coq < 8.8 | 03 April 2019, 13:56:13 UTC |
| 0b1a985 | Raphael Cauderlier | 22 March 2019, 16:15:53 UTC | [build] Ignore shellcheck false alarms | 03 April 2019, 13:54:29 UTC |
| 4f5d906 | Raphael Cauderlier | 03 April 2019, 13:32:35 UTC | [License] Add License headers to all files | 03 April 2019, 13:49:51 UTC |
| a9a08d3 | Raphael Cauderlier | 03 April 2019, 13:31:22 UTC | [License] Assign copyright to Nomadic Labs | 03 April 2019, 13:45:54 UTC |
| 750f2f7 | Seb Mondet | 22 March 2019, 18:17:46 UTC | Make `./configure` work on more platforms Many OSes don't have `bash` in `/bin`, and in this case the script can be easily be made POSIX-compatible (hence `/bin/sh`). | 22 March 2019, 18:17:46 UTC |
| 03bd75c | Julien Tesson | 15 March 2019, 13:20:40 UTC | [Contracts] Adding Mutually calling contracts | 18 March 2019, 14:24:05 UTC |
| 709185b | Raphael Cauderlier | 15 March 2019, 15:16:33 UTC | [Doc]Delete README.md in favor of README.org | 18 March 2019, 14:24:05 UTC |
| 89edb55 | Raphael Cauderlier | 15 March 2019, 15:15:19 UTC | [Doc]Add installation instructions in the README | 18 March 2019, 14:24:05 UTC |
| cc9a0ee | Raphael Cauderlier | 15 March 2019, 07:32:58 UTC | [Build]Add an opam file | 18 March 2019, 14:23:40 UTC |
| a1d6daa | Raphael Cauderlier | 15 March 2019, 07:22:41 UTC | [License] Change (GPLv3 -> MIT) | 18 March 2019, 14:23:40 UTC |
| 515a6a2 | Julien Tesson | 12 March 2019, 15:16:49 UTC | [Doc][Coq][Contracts][Build]Refactoring - add _CoqProject + integration of michocott | 18 March 2019, 14:23:32 UTC |
| 0991155 | Raphael Cauderlier | 11 March 2019, 15:05:43 UTC | [Doc]Update the documentation | 15 March 2019, 15:38:57 UTC |
| 1701b9c | Raphael Cauderlier | 11 March 2019, 12:00:42 UTC | Update TODO list | 15 March 2019, 14:47:54 UTC |
| b660fc5 | Raphael Cauderlier | 09 March 2019, 08:36:46 UTC | Rename "node" into "protocol environment" | 12 March 2019, 14:36:45 UTC |
| c526321 | Raphael Cauderlier | 08 March 2019, 17:01:21 UTC | Remove a useless abstract function | 12 March 2019, 14:36:45 UTC |
| 0b54305 | Raphael Cauderlier | 08 March 2019, 16:20:23 UTC | Update TODO list | 12 March 2019, 14:36:45 UTC |
| 7cd504a | Raphael Cauderlier | 08 March 2019, 16:19:50 UTC | All the functions provided by the environment are now expected to succeed | 12 March 2019, 14:36:45 UTC |
| da384ba | Raphael Cauderlier | 08 March 2019, 14:54:59 UTC | The self function from the environment cannot fail | 12 March 2019, 14:36:45 UTC |
| 3570b0d | Raphael Cauderlier | 08 March 2019, 14:01:29 UTC | Add concrete syntax for lists In Michelson, the concrete syntax for lists is exactly the same as for sets excepts that the elements of sets must be given in ascending order. | 12 March 2019, 14:36:45 UTC |
| 8e6e8a8 | Raphael Cauderlier | 08 March 2019, 13:58:24 UTC | Update the list of possible errors in the documentation | 12 March 2019, 14:36:45 UTC |
| 71ad127 | Raphael Cauderlier | 08 March 2019, 13:58:05 UTC | Add a TODO list | 12 March 2019, 14:36:45 UTC |
| 6b5db67 | Raphael Cauderlier | 08 March 2019, 13:24:48 UTC | Small simplification of the multisig specification | 12 March 2019, 14:36:45 UTC |
| adf4cf5 | Raphael Cauderlier | 07 March 2019, 13:37:34 UTC | Reorder the src/contracts directory | 12 March 2019, 14:36:45 UTC |
| 4fe2dbb | Raphael Cauderlier | 07 March 2019, 10:38:49 UTC | Proof of correctness of the multisig contract | 12 March 2019, 14:36:44 UTC |
| 268bcd3 | Raphael Cauderlier | 07 March 2019, 10:37:54 UTC | Compute a formula equivalent to precond (eval …) | 12 March 2019, 14:36:44 UTC |
| 8624d24 | Raphael Cauderlier | 07 March 2019, 10:36:28 UTC | Prove evaluator’s monotonicity | 12 March 2019, 14:36:44 UTC |
| b736184 | Raphael Cauderlier | 05 March 2019, 10:16:35 UTC | Refactoring: fully separate syntax and semantics | 12 March 2019, 14:36:44 UTC |
| 070db99 | Raphael Cauderlier | 04 March 2019, 09:23:41 UTC | More comparison lemmas | 12 March 2019, 14:36:44 UTC |
| 764ae68 | Raphael Cauderlier | 04 March 2019, 09:21:28 UTC | Update the notations for sequences ";;" is now right associative to help reasoning on contracts in the forward direction. ";;;" does not show up in printing (it is too verbose). | 12 March 2019, 14:36:44 UTC |
| 8f407cc | Raphael Cauderlier | 28 February 2019, 12:30:38 UTC | Add an example of a contract: multisig | 12 March 2019, 14:36:44 UTC |
| 8dfca2a | Raphael Cauderlier | 28 February 2019, 12:26:51 UTC | Define most Michelson macros | 12 March 2019, 14:36:44 UTC |
| 1463e31 | Raphael Cauderlier | 28 February 2019, 12:24:58 UTC | Generalize the types of the IF_* instructions. The documentation is buggy on this point; see https://gitlab.com/tezos/tezos/issues/471 | 12 March 2019, 14:36:44 UTC |
| 4090095 | Raphael Cauderlier | 28 February 2019, 12:23:44 UTC | Fix typing of FAILWITH FAILWITH takes no parameter but takes it argument on the stack. | 12 March 2019, 14:36:44 UTC |
| ad253b1 | Raphael Cauderlier | 28 February 2019, 12:22:14 UTC | Add a NOOP instruction doing nothing (written {} in Micheline) | 12 March 2019, 14:36:44 UTC |
| c1509d2 | Raphael Cauderlier | 28 February 2019, 12:19:27 UTC | Update typing of the CHECK_SIGNATURE instruction | 12 March 2019, 14:36:44 UTC |
| 023bda5 | Raphael Cauderlier | 27 February 2019, 13:23:55 UTC | Rename a variable named I to avoid a name clash with the constructor of True | 12 March 2019, 14:36:44 UTC |
| 31288c7 | Raphael Cauderlier | 27 February 2019, 13:23:25 UTC | Also remove obsolete instructions from the evaluator | 12 March 2019, 14:36:44 UTC |
| 39f508f | Raphael Cauderlier | 27 February 2019, 09:28:53 UTC | Slides update | 12 March 2019, 14:36:44 UTC |
| 727ea56 | Raphael Cauderlier | 17 September 2018, 16:11:10 UTC | Sort instructions by the order in which they are documented | 12 March 2019, 14:36:44 UTC |
| 6f93bf4 | Raphael Cauderlier | 17 September 2018, 16:10:03 UTC | Remove obsolete instructions | 12 March 2019, 14:36:44 UTC |
| 76a7425 | Raphael Cauderlier | 17 September 2018, 16:09:34 UTC | Add some comments | 12 March 2019, 14:36:44 UTC |
| 0911651 | Raphael Cauderlier | 17 September 2018, 14:07:07 UTC | [README] Style | 12 March 2019, 14:36:44 UTC |
| 7fde4f5 | Raphael Cauderlier | 17 September 2018, 14:01:51 UTC | Add some documentation | 12 March 2019, 14:36:44 UTC |
| 9e2186a | Raphael Cauderlier | 17 September 2018, 12:11:09 UTC | Add the slides of today's presentation | 12 March 2019, 14:36:44 UTC |
| ff33b5c | Raphael Cauderlier | 17 September 2018, 12:08:15 UTC | Move code to the src directory | 12 March 2019, 14:36:44 UTC |
| 58dc95c | rafoo | 16 September 2018, 12:32:04 UTC | Add LICENSE | 12 March 2019, 14:36:44 UTC |
| fa36f83 | Raphael Cauderlier | 09 September 2018, 20:15:16 UTC | Update to current status of Michelson | 12 March 2019, 14:36:44 UTC |
| b2146ef | Raphael Cauderlier | 16 August 2018, 18:29:01 UTC | Trailing whitespace | 12 March 2019, 14:36:44 UTC |
| 6e946a3 | Raphael Cauderlier | 24 May 2018, 11:33:55 UTC | Syntax, typing, and operational semantics of the Michelson language in Coq | 12 March 2019, 14:36:44 UTC |
| 3e98c08 | Benjamin Canou | 12 March 2019, 13:33:01 UTC | Initial commit | 12 March 2019, 13:33:01 UTC |
