Commit bdb37468 authored by Ralf Jung's avatar Ralf Jung

Add some comments explaining what these files do

Just because we don't have such comments for other files, doesn't mean we can't
start applying some best practices.
parent dbe52472
(** An axiomatization of evaluation-context based languages, including a proof
that this gives rise to a "language" in the Iris sense. *)
From iris.algebra Require Export base. From iris.algebra Require Export base.
From iris.program_logic Require Export language. From iris.program_logic Require Export language.
......
(** Some derived lemmas for ectx-based languages *)
From iris.program_logic Require Export ectx_language weakestpre lifting. From iris.program_logic Require Export ectx_language weakestpre lifting.
From iris.program_logic Require Import ownership. From iris.program_logic Require Import ownership.
......
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