Commit 9f9bad3e authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents e2458a73 15be7b25
(** This file is essentially a bunch of testcases. *) (** This file is essentially a bunch of testcases. *)
Require Import program_logic.ownership. Require Import program_logic.ownership.
Require Import heap_lang.substitution heap_lang.tactics heap_lang.notation. From heap_lang Require Import substitution tactics notation.
Import uPred. Import uPred.
Module LangTests. Module LangTests.
......
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