Commit 37262a82 authored by Ralf Jung's avatar Ralf Jung

fix build on old versions of Coq

parent dddd0fd1
From iris.algebra Require Export cmra.
From iris.algebra Require Import list.
From iris.base_logic Require Import base_logic.
Import stdpp.list. (* Make sure we use those names. FIXME: remove when we drop Coq 8.9 support. *)
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ _ !_ /.
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment