From 210a25decda2b3e20d861c840cfb0942e010aae0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= <pierre-marie.pedrot@inria.fr>
Date: Tue, 17 Dec 2024 15:25:31 +0100
Subject: [PATCH] Adapt w.r.t. coq/coq#19943.

---
 src/declare_translation.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/declare_translation.ml b/src/declare_translation.ml
index 9ba27e1..4dd541d 100644
--- a/src/declare_translation.ml
+++ b/src/declare_translation.ml
@@ -216,7 +216,7 @@ and declare_module ~opaque_access ?(continuation = ignore) ?name arity mb  =
   debug_string [`Module] "--> declare_module";
   let open Declarations in
   let mp = mb.mod_mp in
-  match mb.mod_expr, mb.mod_type with
+  match Declareops.mod_expr mb, mb.mod_type with
   | Algebraic _, NoFunctor fields
   | FullStruct, NoFunctor fields ->
      let id = id_of_module_path mp in
@@ -299,7 +299,7 @@ and declare_module ~opaque_access ?(continuation = ignore) ?name arity mb  =
        end
      | (lab, SFBmodule mb') when
           match mb'.mod_type with NoFunctor _ ->
-            (match mb'.mod_expr with FullStruct | Algebraic _ -> true | _ -> false)
+            (match Declareops.mod_expr mb' with FullStruct | Algebraic _ -> true | _ -> false)
           | _ -> false
         ->
         declare_module ~opaque_access ~continuation arity mb'