Verified Commit 7a581d15 authored by Tej Chajed's avatar Tej Chajed
Browse files

Use the new proofmode entry file

parent af8a5c31
From iris.program_logic Require Import adequacy.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From spacelang Require Import wp_state_interp.
(* This module proves the adequacy (i.e. the soundness) of Iris for
......
From iris.algebra Require Export auth numbers.
From iris.base_logic.lib Require Import own.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
(* from https://gitlab.inria.fr/gmevel/iris-time-proofs/-/blob/master/theories/Auth_nat.v *)
......
From stdpp Require Import gmap gmultiset.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From spacelang Require Import stdpp.
(* This file defines a small set of hypotheses about locations and blocks.
......
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
(* A fancy update with access to the state interpretation predicate. *)
......
From iris.algebra Require Import auth gmap gmultiset.
From iris.base_logic.lib Require Import gen_heap.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From spacelang Require Import hypotheses successors predecessors.
From spacelang Require Import stdpp.
From spacelang Require iris.
......
From iris.algebra Require Import gmap gmultiset.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From spacelang Require Import stdpp hypotheses.
(* This file contains mathematical results about the interplay between
......
From iris.proofmode Require Export coq_tactics reduction.
From iris.proofmode Require Export tactics.
From iris.proofmode Require Export proofmode.
From iris.program_logic Require Import atomic.
From iris Require Import spec_patterns intro_patterns.
From spacelang Require Export ph wp instances notation.
......
From iris.proofmode Require Export coq_tactics reduction.
From iris.proofmode Require Export tactics.
From iris.proofmode Require Export proofmode.
From iris.program_logic Require Import atomic.
From iris Require Import spec_patterns intro_patterns.
From spacelang Require Export ph wp instances notation.
......
From iris.proofmode Require Export coq_tactics reduction.
From iris.proofmode Require Export tactics.
From iris.proofmode Require Export proofmode.
From iris.program_logic Require Import atomic.
From iris Require Import spec_patterns intro_patterns.
From spacelang Require Export ph rc wp proofmode.
......
From stdpp Require Import gmap gmultiset.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From spacelang Require Import stdpp hypotheses gset_fixpoint.
(* This file contains mathematical results about the notions of successor,
......
......@@ -2,7 +2,7 @@ From iris.algebra Require Export dfrac.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Export ectx_lifting.
From iris.proofmode Require Export tactics.
From iris.proofmode Require Export proofmode.
From spacelang Require Export iris stdpp.
From spacelang Require Export authnat.
From spacelang Require Export hypotheses successors predecessors ph.
......
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