Skip to content

saved predicates: use ofe_fun, not ofe_mor

Ralf Jung requested to merge ralf/saved_prop into master

The only two known users of this saved predicates (iris-atomic and @amintimany) only need discrete premises for their saved predicates; this makes the API easier to use for them.

Edited by Ralf Jung

Merge request reports