From 4965e20bafc2001b0950e668abd4726fa6a19be6 Mon Sep 17 00:00:00 2001 From: Dario Halilovic Date: Sun, 13 Sep 2026 15:06:16 +0200 Subject: [PATCH 1/2] fix: fix Summary.Ref failures on master --- examples/Tour.v | 2 ++ src/module_manager.ml | 4 ++++ 2 files changed, 6 insertions(+) diff --git a/examples/Tour.v b/examples/Tour.v index ac546fc..839ec5e 100644 --- a/examples/Tour.v +++ b/examples/Tour.v @@ -252,6 +252,8 @@ 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 + open Summary.Ref + let inc () = value := !value + 1 let print () = 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 From 6e711937af067d5d912157d95fa4b82fb370ca07 Mon Sep 17 00:00:00 2001 From: Dario Halilovic Date: Sun, 13 Sep 2026 21:13:51 +0200 Subject: [PATCH 2/2] fix: fix tour failing on Summary.Ref This make camltac-examples compile on both 9.2 (CI) and dev. This fix is temporary however, and we should find a better way. --- examples/Tour.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/examples/Tour.v b/examples/Tour.v index 839ec5e..402c5f0 100644 --- a/examples/Tour.v +++ b/examples/Tour.v @@ -250,9 +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 - - open Summary.Ref + 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