- Move
IntoVal
,AsVal
,Atomic
,AsRecV
, andPureExec
instances to their own fileheap_lang.class_instances
- Move
inv_head_step
tactic andhead_step
instances (now part of new hint databasehead_step
) toheap_lang.tactics
I ported Iron so that it uses Iris's HeapLang instead of forking it. Iron defines its own WP (in a linear rather than affine logic), but should reuse all HeapLang class instances and tactics. Hence, they should not be in primitive_laws
.