Commit ec47a113 authored by Ralf Jung's avatar Ralf Jung

update iris to use stdpp

parent 2f018fc2
Pipeline #3829 failed with stage
in 14 minutes and 13 seconds
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq b0418bd57b9341dbf5e58669c689201daa561bd7
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 50a1b62bfaaa3619621b33b0254865e66ecc4fc9
From Coq Require Import Min.
From iris.prelude Require Import coPset.
From stdpp Require Import coPset.
From iris.algebra Require Import cmra_big_op gmap frac agree.
From iris.algebra Require Import csum excl auth.
From iris.base_logic Require Import big_op lib.fractional.
......
From iris.program_logic Require Export language ectx_language ectxi_language.
From iris.prelude Require Export strings.
From iris.prelude Require Import gmap.
From stdpp Require Export strings.
From stdpp Require Import gmap.
Set Default Proof Using "Type".
Open Scope Z_scope.
......
From iris.prelude Require Import gmap.
From stdpp Require Import gmap.
From iris.program_logic Require Export hoare.
From iris.program_logic Require Import adequacy.
From lrust.lang Require Import tactics.
......
From iris.prelude Require Import fin_maps.
From stdpp Require Import fin_maps.
From lrust.lang Require Export lang.
Set Default Proof Using "Type".
......
From iris.algebra Require Import frac.
From iris.prelude Require Export gmultiset strings.
From stdpp Require Export gmultiset strings.
From iris.base_logic.lib Require Export invariants.
From iris.base_logic.lib Require Import boxes fractional.
Set Default Proof Using "Type".
......
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