Commit c913924f authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Useless Require.

parent ddd48268
From iris.base_logic.lib Require Export invariants. From iris.base_logic.lib Require Export invariants.
From iris.algebra Require Export gmap gset coPset. From iris.algebra Require Import gset coPset.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Import uPred. Import uPred.
......
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