Commit dbe9e6ea authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso Committed by Ralf Jung

Clarify use of Require

parent e16680d5
From iris.proofmode Require Export ltac_tactics.
(* This [Require Import] is not a no-op: it exports typeclass instances from
these files. *)
From iris.proofmode Require Import class_instances_bi class_instances_sbi frame_instances modality_instances.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment