From 675a023ed0a8c316d75d2565389f33f1749658c0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Aug 2022 09:11:57 -0400
Subject: [PATCH] more coqdoc

---
 iris_unstable/algebra/list.v          | 2 +-
 iris_unstable/algebra/monotone.v      | 2 +-
 iris_unstable/base_logic/algebra.v    | 2 +-
 iris_unstable/base_logic/mono_list.v  | 2 +-
 iris_unstable/heap_lang/interpreter.v | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/iris_unstable/algebra/list.v b/iris_unstable/algebra/list.v
index 36fa11fd2..0afcf8c30 100644
--- a/iris_unstable/algebra/list.v
+++ b/iris_unstable/algebra/list.v
@@ -1,4 +1,4 @@
-(* This file is still experimental. See its tracking issue
+(** This file is still experimental. See its tracking issue
 https://gitlab.mpi-sws.org/iris/iris/-/issues/407 for details on remaining
 issues before stabilization. *)
 From stdpp Require Export list.
diff --git a/iris_unstable/algebra/monotone.v b/iris_unstable/algebra/monotone.v
index 9ca5e3cb9..068fed672 100644
--- a/iris_unstable/algebra/monotone.v
+++ b/iris_unstable/algebra/monotone.v
@@ -1,4 +1,4 @@
-(* This file is still experimental. See its tracking issue
+(** This file is still experimental. See its tracking issue
 https://gitlab.mpi-sws.org/iris/iris/-/issues/414 for details on remaining
 issues before stabilization. *)
 
diff --git a/iris_unstable/base_logic/algebra.v b/iris_unstable/base_logic/algebra.v
index 511d95f55..adb10e2f8 100644
--- a/iris_unstable/base_logic/algebra.v
+++ b/iris_unstable/base_logic/algebra.v
@@ -1,4 +1,4 @@
-(* This is just an integration file for [iris_staging.algebra.list];
+(** This is just an integration file for [iris_staging.algebra.list];
 both should be stabilized together. *)
 From iris.algebra Require Import cmra.
 From iris.unstable.algebra Require Import list monotone.
diff --git a/iris_unstable/base_logic/mono_list.v b/iris_unstable/base_logic/mono_list.v
index b86424c9c..f8db43cce 100644
--- a/iris_unstable/base_logic/mono_list.v
+++ b/iris_unstable/base_logic/mono_list.v
@@ -1,4 +1,4 @@
-(* This file is still experimental. See its tracking issue
+(** This file is still experimental. See its tracking issue
 https://gitlab.mpi-sws.org/iris/iris/-/issues/439 for details on remaining
 issues before stabilization. *)
 (** Ghost state for a append-only list, wrapping the [mono_listR] RA. This
diff --git a/iris_unstable/heap_lang/interpreter.v b/iris_unstable/heap_lang/interpreter.v
index 27d398447..8d0771a77 100644
--- a/iris_unstable/heap_lang/interpreter.v
+++ b/iris_unstable/heap_lang/interpreter.v
@@ -1,4 +1,4 @@
-(* This file is still experimental. See its tracking issue
+(** This file is still experimental. See its tracking issue
 https://gitlab.mpi-sws.org/iris/iris/-/issues/405 for details on remaining
 issues before stabilization. *)
 
-- 
GitLab