diff --git a/library/summary.ml b/library/summary.ml index 17296e87c6fb..758b636dc122 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -216,14 +216,4 @@ let ref ?(stage=Stage.Interp) ?(local=false) ~name x = in r -module Local = struct - -type 'a local_ref = 'a ref - -let ref ?stage ~name x = ref ?stage ~name ~local:true x -let (!) = (!) -let (:=) = (:=) - -end - let dump = Dyn.dump diff --git a/library/summary.mli b/library/summary.mli index 71a2d29045c1..a77bc189b521 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -67,15 +67,6 @@ val declare_summary_tag : string -> ?make_marshallable:('a -> 'a) -> 'a summary_ val ref : ?stage:Stage.t -> ?local:bool -> name:string -> 'a -> 'a ref val ref_tag : ?stage:Stage.t -> name:string -> 'a -> 'a ref * 'a Dyn.tag -module Local : sig - - type 'a local_ref = 'a ref - val ref : ?stage:Stage.t -> name:string -> 'a -> 'a local_ref - val (:=) : 'a local_ref -> 'a -> unit - val (!) : 'a local_ref -> 'a - -end [@@ocaml.deprecated "Use [Summary.ref ~local:true]"] - (** Special summary for ML modules. This summary entry is special because its unfreeze may load ML code and hence add summary entries. Thus is has to be recognizable, and handled properly. diff --git a/test-suite/misc/non-marshalable-state/src/good.mlg b/test-suite/misc/non-marshalable-state/src/good.mlg index 260e6339c9f3..bb422ee57ef7 100644 --- a/test-suite/misc/non-marshalable-state/src/good.mlg +++ b/test-suite/misc/non-marshalable-state/src/good.mlg @@ -2,7 +2,7 @@ DECLARE PLUGIN "coq-test-suite.good" { -let state = Summary.Local.ref +let state = Summary.ref ~local:true ~name:"elpi-compiler-cache" None @@ -10,7 +10,6 @@ let state = Summary.Local.ref VERNAC COMMAND EXTEND magic CLASSIFIED AS SIDEFF | [ "magic" ] -> { - let open Summary.Local in state := Some (fun () -> ()) } END