From 74858b88a2ff08e6e708ec610dc1143abd299a1d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 12 Aug 2019 13:50:03 +0200
Subject: [PATCH] comment examples

---
 tests/one_shot.v      | 3 +++
 tests/one_shot_once.v | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/tests/one_shot.v b/tests/one_shot.v
index 01159f1a7..dd9f08ed0 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -6,6 +6,9 @@ From iris.proofmode Require Import tactics.
 From iris.heap_lang.lib Require Import par.
 Set Default Proof Using "Type".
 
+(** This is the introductory example from the "Iris from the Ground Up" journal
+paper. *)
+
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref NONE in (
   (* tryset *) (λ: "n",
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 986b021ee..ad8ea8147 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -6,6 +6,9 @@ From iris.proofmode Require Import tactics.
 From iris.heap_lang.lib Require Import par.
 Set Default Proof Using "Type".
 
+(** This is the introductory example from Ralf's PhD thesis.
+The difference to [one_shot] is that [set] asserts to be called only once. *)
+
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref NONE in (
   (* set *) (λ: "n",
-- 
GitLab