Commit 705d580e authored by Ralf Jung's avatar Ralf Jung

*oops* forgot to fix imports

parent 31d90720
Require Export barrier.heap_lang.
Require Export heap_lang.heap_lang.
Require Import prelude.fin_maps.
Import heap_lang.
......
Require Import prelude.gmap iris.lifting.
Require Export iris.weakestpre barrier.heap_lang_tactics.
Require Export iris.weakestpre heap_lang.heap_lang_tactics.
Import uPred.
Import heap_lang.
Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
......
Require Export barrier.heap_lang barrier.lifting.
Require Export heap_lang.heap_lang heap_lang.lifting.
Import uPred.
Import heap_lang.
......
(** This file is essentially a bunch of testcases. *)
Require Import modures.logic.
Require Import barrier.lifting barrier.sugar.
Require Import heap_lang.lifting heap_lang.sugar.
Import heap_lang.
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