Beginning of dep translation of the translator
In this branch there are:
- Some changes on the interpreter, to type the term
ks
; - Some dependent definitions for the translator;
- Some equality proofs on these dependent definitions;
- New axioms to reason about existential matches in the environment file.
These axioms are not yet sufficient for all our code examples as I will also need to modify coq-of-ocaml
to remove unused existential variables.
Edited by Guillaume Claret