diff --git a/opam.pins b/opam.pins index b496f750fc3ef03c16bcba873827a7483400ccee..607c346aae6510fc42352c82e3ae8e7e527ac244 100644 --- a/opam.pins +++ b/opam.pins @@ -1 +1 @@ -coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 02bc52b4d905eb635940ff8545d59676ad44ea8c +coq-iris https://gitlab.mpi-sws.org/FP/iris-coq c3dde6181d7d99007fd584d23a5dc3e859b47765 diff --git a/theories/lang/lang.v b/theories/lang/lang.v index 70f6f9069c405e64868a9cb9feb8b2948efe6ab0..9ec5db995b6bd7f7bcbc54a03ef73c940e13df7f 100644 --- a/theories/lang/lang.v +++ b/theories/lang/lang.v @@ -1,5 +1,5 @@ From iris.program_logic Require Export language ectx_language ectxi_language. -From stdpp Require Export strings. +From fast_string Require Export fast_string_lib. From stdpp Require Import gmap. Set Default Proof Using "Type". diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v index 4684b65d115f0ae967368e629234dcd33e5d3632..89a403a30735f39c5fb16fd8a9af9bf212460918 100644 --- a/theories/lifetime/lifetime_sig.v +++ b/theories/lifetime/lifetime_sig.v @@ -1,5 +1,6 @@ From iris.algebra Require Import frac. -From stdpp Require Export gmultiset strings. +From stdpp Require Export gmultiset. +From fast_string Require Export fast_string_lib. From iris.base_logic.lib Require Export invariants. From iris.base_logic.lib Require Import boxes fractional. Set Default Proof Using "Type".