From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

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

(limited to 'lib/store.mli')

diff --git a/lib/store.mli b/lib/store.mli
new file mode 100644
index 00000000..5df0c99a
--- /dev/null
+++ b/lib/store.mli
@@ -0,0 +1,25 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*** This module implements an "untyped store", in this particular case we
+        see it as an extensible record whose fields are left unspecified. ***)
+
+type t
+
+module Field : sig
+  type 'a field = {
+    set : 'a -> t -> t ;
+    get : t -> 'a option ;
+    remove : t -> t 
+  }
+  type 'a t = 'a field
+end
+
+val empty : t
+
+val field : unit -> 'a Field.field
-- 
cgit v1.2.3