Skip to content
Snippets Groups Projects
Commit fec84da6 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove useless import.

parent 9200cc77
No related branches found
No related tags found
No related merge requests found
From stdpp Require Import namespaces.
From iris.program_logic Require Export weakestpre.
From iris.algebra Require Import gmap auth agree gset coPset.
From iris.base_logic.lib Require Import wsat.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment