Tactics.v 263 Bytes
Newer Older
1
From iris_time.heap_lang Require Export lang tactics.
2 3 4

Ltac prim_step :=
  lazymatch goal with
5 6 7
  | |- prim_step ?e _ _ _ _ _ =>
      reshape_expr true e ltac:(fun K e' =>
        esplit with K e' _ ; [ reflexivity | reflexivity | ] ; econstructor
8
      )
9
  end.