Skip to content
Snippets Groups Projects
Commit e87b3f2d authored by Ralf Jung's avatar Ralf Jung
Browse files

fix imports

parent 39fad8e8
No related branches found
No related tags found
No related merge requests found
Pipeline #115156 passed
From orc11 Require Export base. From gpfsl.orc11 Require Export base.
Require Import iris.bi.lib.fractional. Require Import iris.bi.lib.fractional.
From lrust.lifetime Require Export lifetime_sig. From lrust.lifetime Require Export lifetime_sig.
From lrust.lifetime.model Require definitions primitive accessors faking borrow From lrust.lifetime.model Require definitions primitive accessors faking borrow
......
...@@ -2,7 +2,7 @@ From stdpp Require Export gmultiset strings. ...@@ -2,7 +2,7 @@ From stdpp Require Export gmultiset strings.
From iris.algebra Require Import frac. From iris.algebra Require Import frac.
From iris.base_logic.lib Require Export invariants. From iris.base_logic.lib Require Export invariants.
From iris.bi Require Import fractional. From iris.bi Require Import fractional.
From orc11 Require Import base. From gpfsl.orc11 Require Import base.
From gpfsl.base_logic Require Export vprop. From gpfsl.base_logic Require Export vprop.
From iris.proofmode Require Import proofmode. From iris.proofmode Require Import proofmode.
......
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