Skip to content
Snippets Groups Projects
Commit 675a023e authored by Ralf Jung's avatar Ralf Jung
Browse files

more coqdoc

parent c9223a52
No related branches found
No related tags found
No related merge requests found
(* 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.
......
(* 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. *)
......
(* 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.
......
(* 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
......
(* 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. *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment