tactics.v 427 Bytes
Newer Older
1
From iris.proofmode Require Export ltac_tactics.
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
2 3
(* This [Require Import] is not a no-op: it exports typeclass instances from
these files. *)
4 5 6 7
From iris.proofmode Require Import class_instances class_instances_later
  class_instances_updates class_instances_embedding
  class_instances_plainly class_instances_internal_eq.
From iris.proofmode Require Import frame_instances modality_instances.
8
From iris Require Import options.