ocaml-gospel / ortac

Runtime assertion checking based on Gospel specifications
https://ocaml-gospel.github.io/ortac/
MIT License
36 stars 10 forks source link

[wrapper] Add support for `old` operator #201

Open n-osborne opened 6 months ago

n-osborne commented 6 months ago

This issue proposes to add support for the old operator in the wrapper plugin.

For now, terms containing an old operator are simply skipped.

Clément has already some code here using the marshalling technic described in his thesis and the paper here. That could be a very good starting point.

There is some rebasing to do to begin with.