From 674b22d21aed9e5c00631b1b5f2a335a1ed91c7f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 22 Feb 2017 15:02:31 +0100
Subject: [PATCH] Use fast_string.

---
 opam.pins                        | 2 +-
 theories/lang/lang.v             | 2 +-
 theories/lifetime/lifetime_sig.v | 3 ++-
 3 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/opam.pins b/opam.pins
index b496f750..607c346a 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 70f6f906..9ec5db99 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 4684b65d..89a403a3 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".
-- 
GitLab