From bdb37468ad4159745e2cfe1e0a17b0ffeae97a7a Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 30 Mar 2016 09:06:18 +0200 Subject: [PATCH] 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. --- program_logic/ectx_language.v | 2 ++ program_logic/ectx_weakestpre.v | 1 + 2 files changed, 3 insertions(+) diff --git a/program_logic/ectx_language.v b/program_logic/ectx_language.v index 2cae45d14..8e9fa62e8 100644 --- a/program_logic/ectx_language.v +++ b/program_logic/ectx_language.v @@ -1,3 +1,5 @@ +(** 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.program_logic Require Export language. diff --git a/program_logic/ectx_weakestpre.v b/program_logic/ectx_weakestpre.v index c28eff3f4..820ff411a 100644 --- a/program_logic/ectx_weakestpre.v +++ b/program_logic/ectx_weakestpre.v @@ -1,3 +1,4 @@ +(** Some derived lemmas for ectx-based languages *) From iris.program_logic Require Export ectx_language weakestpre lifting. From iris.program_logic Require Import ownership. -- GitLab