Commit 5213177f authored by Ralf Jung's avatar Ralf Jung
Browse files

algebra.sts as the wrong file, the affected lemmas are in base_logic.lib.sts...

algebra.sts as the wrong file, the affected lemmas are in base_logic.lib.sts (already fixed by Robbert)
parent 4c38ac07
From iris.prelude Require Export set. From iris.prelude Require Export set.
From iris.algebra Require Export cmra. From iris.algebra Require Export cmra.
From iris.algebra Require Import dra. From iris.algebra Require Import dra.
(* FIXME: This file needs a 'Proof Using' hint, but the default we use Set Default Proof Using "Type*".
everywhere makes for lots of extra ssumptions. *)
Local Arguments valid _ _ !_ /. Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /. Local Arguments op _ _ !_ !_ /.
Local Arguments core _ _ !_ /. Local Arguments core _ _ !_ /.
......
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