Michelson: remove the infinite cases in dep_step_eq (!431) · Merge requests · Formal Land / Coq Tezos of OCaml 💫 · 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 first breaking change window begins 2024-04-22 09:00UTC and ends 2024-04-24 22:00UTC.

Guillaume Claret requested to merge guillaume-claret@remove-the-slow-cases-from-dep_step_eq into master Apr 21, 2022

Some cases in the proof of https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/proofs/script_interpreter#dep_step_eq were too slow (probably infinite). This MR fixes that and verifies a few more cases.

Fix https://gitlab.com/nomadic-labs/coq-tezos-of-ocaml/-/issues/116

Edited Apr 21, 2022 by Guillaume Claret