From 6fefa83fb63e6fe81cebf012cd3b86a8d22a209d Mon Sep 17 00:00:00 2001
From: Yann Leray <yann.leray@inria.fr>
Date: Mon, 5 Feb 2024 12:19:36 +0100
Subject: [PATCH] Adapt to coq/coq#18038 (rewrite rules)

---
 src/coq_elpi_HOAS.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
index 661b9720b..edfe7fcef 100644
--- a/src/coq_elpi_HOAS.ml
+++ b/src/coq_elpi_HOAS.ml
@@ -3492,6 +3492,7 @@ let rec in_elpi_module_item ~depth path state (name, item) =
       [Gref (GlobRef.ConstRef (Constant.make2 path name))]
   | SFBmind { mind_packets } ->
       CList.init (Array.length mind_packets) (fun i -> Gref (GlobRef.IndRef (MutInd.make2 path name,i)))
+  | SFBrules _ -> nYI "rewrite rules"
   | SFBmodule ({ mod_mp; mod_type = NoFunctor _ } as b) -> [Module (mod_mp,in_elpi_module ~depth state b) ]
   | SFBmodule { mod_mp; mod_type = MoreFunctor _ as l } -> [Functor(mod_mp,functor_params l)]
   | SFBmodtype { mod_mp; mod_type = NoFunctor _ }  -> [ModuleType mod_mp]
@@ -3524,6 +3525,7 @@ let rec in_elpi_modty_item (name, item) = match item with
       [ Label.to_string name ]
   | Declarations.SFBmind _ ->
       [ Label.to_string name ]
+  | Declarations.SFBrules _ -> nYI "rewrite rules"
   | Declarations.SFBmodule mb -> in_elpi_modty mb
   | Declarations.SFBmodtype _ -> []