I have a Coq file Expr.v that gets extracted to expr.ml, and I have a compiler front end that produces values for the types in expr.ml. Is there a way to "un-extract" and pretty-print these expr.ml OCaml values to the datatypes defined in Expr.v?
the closest you have in this direction is probably CoqOfOCaml, but extraction changes names a lot, so would be surprised to see a full reconnection.
Last updated: Apr 19 2024 at 18:01 UTC