From a181837b5e36b2a0b824472cdc42df8866775caf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 1 Jun 2018 10:13:13 +0200
Subject: [PATCH] Comments in tests/ipm_paper.

---
 tests/ipm_paper.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 38ad33dc6..930c7dec4 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -1,3 +1,8 @@
+(** This file contains the examples from the paper:
+
+Interactive Proofs in Higher-Order Concurrent Separation Logic
+Robbert Krebbers, Amin Timany and Lars Birkedal
+POPL 2017 *)
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export hoare.
-- 
GitLab