From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 clib/store.mli | 43 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)
 create mode 100644 clib/store.mli

(limited to 'clib/store.mli')

diff --git a/clib/store.mli b/clib/store.mli
new file mode 100644
index 00000000..0c2b2e08
--- /dev/null
+++ b/clib/store.mli
@@ -0,0 +1,43 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(*** This module implements an "untyped store", in this particular case we
+        see it as an extensible record whose fields are left unspecified. ***)
+
+module type S =
+sig
+  type t
+  (** Type of stores *)
+
+  type 'a field
+  (** Type of field of such stores *)
+
+  val empty : t
+  (** Empty store *)
+
+  val set : t -> 'a field -> 'a -> t
+  (** Set a field *)
+
+  val get : t -> 'a field -> 'a option
+  (** Get the value of a field, if any *)
+
+  val remove : t -> 'a field -> t
+  (** Unset the value of the field *)
+
+  val merge : t -> t -> t
+  (** [merge s1 s2] adds all the fields of [s1] into [s2]. *)
+
+  val field : unit -> 'a field
+  (** Create a new field *)
+
+end
+
+module Make () : S
+(** Create a new store type. *)
-- 
cgit v1.2.3