aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/store.mli
blob: 5df0c99a7629094c2e4b95f8b712cf62a400106c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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