Update: remove unused existential variables
In this MR, we change the output of coq-of-ocaml
so that existential variables which are not in use are not added to the cast_exists
casts. This helps to infer the values for the existential types, as only one answer is generally possible. This also reduces slightly the verbosity of the code, eliminating dead code.
As an example, we complete the proof of dep_cost_of_instr_eq
https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/proofs/script_interpreter_defs#dep_cost_of_instr_eq. Here there is some documentation about eliminating the casts: https://gitlab.com/foobar-land/roadmap-coq-tezos-of-ocaml/-/wikis/home#eliminate-cast-and-cast_exists
Finally, doing this proof we discovered some differences between the simulation and the actual code and fixed them (most are due to new code updates).