Skip to content
GitLab
Commit 7b90e259 authored by Ike Mulder's avatar Ike Mulder
Browse files

Fixed verify_tac depending on iris.heap_lang.

parent be389c78
Pipeline #74233 passed with stages
in 32 minutes and 14 seconds
Hide whitespace changes
Inline Side-by-side
diaframe/steps/verify_tac.v
View file @ 7b90e259
From diaframe Require Import util_classes.
From diaframe.steps Require Import tactics.
From iris.heap_lang Require Import proofmode.
From iris.base_logic.lib Require Import iprop own.
From iris.proofmode Require Import proofmode.
From Coq.Program Require Import Tactics.
......
Supports Markdown
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