Commit 41b5418a authored by Léon Gondelman's avatar Léon Gondelman

fix compilation

parent 73e57afc
......@@ -2,7 +2,7 @@ From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
From iris.bi Require Import big_op.
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
From iris_c.c_translation Require Import monad translation proofmode notation.
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.lib Require Import locking_heap U.
Section test.
......@@ -29,7 +29,7 @@ Section test.
Qed.
Lemma test4 (l : loc) (v1 v2: val) :
l C v1 - awp ( l = ret v2) True (λ v, v = v2 l C[LLvl] v2).
l C v1 - awp ( l = a_ret v2) True (λ v, v = v2 l C[LLvl] v2).
Proof.
iIntros "Hl1". vcg_solver. auto.
Qed.
......
......@@ -2,7 +2,7 @@ From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
From iris.bi Require Import big_op.
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
From iris_c.c_translation Require Import monad translation notation proofmode derived.
From iris_c.c_translation Require Import monad translation proofmode derived.
From iris_c.lib Require Import locking_heap U.
Definition incr : val := λ: "l",
......
......@@ -2,7 +2,7 @@ From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
From iris.bi Require Import big_op.
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
From iris_c.c_translation Require Import monad translation notation proofmode derived.
From iris_c.c_translation Require Import monad translation proofmode derived.
From iris_c.lib Require Import locking_heap U.
Section tests_vcg.
......
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