Represent mutez using the builtin int63 type (!112) · Merge requests · Nomadic Labs / Mi-Cho-Coq · GitLab

The 17.0 major release is coming on May 16, 2024! This version brings many exciting improvements to GitLab, but also removes some deprecated features. We are introducing three breaking change windows during which we expect breaking changes to be deployed to GitLab.com. You can read more about it on our blogpost . The second breaking change window begins 2024-04-29 09:00 UTC and ends 2024-05-01 22:00 UTC.

Raphaël Cauderlier requested to merge rafoo@builtin_mutez into dev Mar 10, 2021

In Coq 8.10, builtin support for int63 has been added. This is exactly the type needed to represent mutez.

This MR:

changes the representation of mutez
removes the now unused module "int64bv"
drops support for Coq < 8.10
adapts the contract proofs for the new implementation. In particular the proof of vesting_tez has been rewritten.