Commit 674b22d2 authored by Robbert Krebbers's avatar Robbert Krebbers

Use fast_string.

parent 25c37eb0
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 02bc52b4d905eb635940ff8545d59676ad44ea8c
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq c3dde6181d7d99007fd584d23a5dc3e859b47765
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".
......
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".
......
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