Library iris.proofmode.proofmode

The main proofmode file taht everyone should import. Unless you are working with the guts of the proofmode, do not import any other file from this folder!
From iris.proofmode Require Export ltac_tactics.
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.
From iris.prelude Require Import options.