diff --git a/examples/Tour.v b/examples/Tour.v index ac546fc..402c5f0 100644 --- a/examples/Tour.v +++ b/examples/Tour.v @@ -250,7 +250,9 @@ For example, here's an implementation of a simple mutable counter that follows b |*) Camltac Module Counter := ocaml:{{ - let value = Summary.ref ~stage:Interp ~name:"counter" 0 + let value: int ref = + (* FIXME: Rocq 9.3 recently made this type abstract. *) + Obj.magic (Summary.ref ~stage:Interp ~name:"counter" 0) let inc () = value := !value + 1 diff --git a/src/module_manager.ml b/src/module_manager.ml index 2f54d09..536e5c2 100644 --- a/src/module_manager.ml +++ b/src/module_manager.ml @@ -10,6 +10,10 @@ type state = packing_module: string option; } +[%%if rocq >= (9, 3)] +open Summary.Ref +[%%endif] + let state = Summary.ref ~stage:Synterp