diff options
| author | Pierre-Marie Pédrot | 2021-01-22 17:04:19 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-22 17:35:40 +0100 |
| commit | 7a25cc5f29a16e05a3289ad66dca2817b63649ef (patch) | |
| tree | 5cc6b6a761225d2f1a898e5a4d27edcc76f67fb6 /library/summary.mli | |
| parent | 7d5618684ef17fbb34246f041b3426d42825b85a (diff) | |
Properly implement local references in Summary.
Diffstat (limited to 'library/summary.mli')
| -rw-r--r-- | library/summary.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/summary.mli b/library/summary.mli index 7c5e1bee6f..a6f94a49ae 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -53,7 +53,7 @@ val ref_tag : ?freeze:(marshallable:bool -> 'a -> 'a) -> name:string -> 'a -> 'a module Local : sig type 'a local_ref - val ref : ?freeze:('a -> 'a) -> name:string -> 'a -> 'a local_ref + val ref : name:string -> 'a -> 'a local_ref val (:=) : 'a local_ref -> 'a -> unit val (!) : 'a local_ref -> 'a |