Commit 3c7620d2 authored by Ralf Jung's avatar Ralf Jung
Browse files

update dependencies

parent 78cc584f
......@@ -11,6 +11,6 @@ install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris_time" ]
depends: [
"coq" { (>= "8.10.2" & < "8.13~") | (= "dev") }
"coq-iris" { (= "dev.2021-06-26.0.c7fcd140") | (= "dev") }
"coq-iris" { (= "dev.2021-07-28.0.3424ace5") | (= "dev") }
"coq-tlc" { (= "20200328") | (= "dev") }
]
From iris Require Export algebra.auth algebra.numbers.
From iris Require Import algebra.excl base_logic.lib.own proofmode.tactics.
From iris Require Import algebra.excl base_logic.lib.own proofmode.proofmode.
Section Auth_max_nat.
Context `{inG Σ (authR max_natUR)}.
......
From iris Require Export algebra.auth algebra.numbers.
From iris Require Import base_logic.lib.own proofmode.tactics.
From iris Require Import base_logic.lib.own proofmode.proofmode.
Notation "'●nat' n" := (auth_auth (A:=natUR) (DfracOwn 1%Qp) n%nat) (at level 20).
Notation "'◯nat' n" := (auth_frag (A:=natUR) n%nat) (at level 20).
......
From iris.program_logic Require Export weakestpre adequacy.
From iris.algebra Require Import auth.
From iris_time.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
Set Default Proof Using "Type".
Class heapGpreS Σ := HeapGpreS {
......
From iris.program_logic Require Export weakestpre.
From iris_time.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From iris_time.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......
......@@ -4,7 +4,7 @@ From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting.
From iris_time.heap_lang Require Export lang.
From iris_time.heap_lang Require Import tactics.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From stdpp Require Import fin_maps.
Set Default Proof Using "Type".
......
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import coq_tactics reduction.
From iris.proofmode Require Export tactics.
From iris.proofmode Require Export proofmode.
From iris_time.heap_lang Require Export tactics lifting.
From iris_time.heap_lang Require Import notation.
Set Default Proof Using "Type".
......
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