From 78b48d223f736d7a2d3bc9a0eb739310b6e201dc Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Sun, 25 Jun 2023 23:31:50 +0200
Subject: [PATCH] Adapt to coq/coq#17754

---
 src/coq_elpi_arg_HOAS.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml
index 974ce46cb..54db82582 100644
--- a/src/coq_elpi_arg_HOAS.ml
+++ b/src/coq_elpi_arg_HOAS.ml
@@ -205,7 +205,7 @@ let univpoly_of ~poly ~cumulative =
     if notations != [] then CErrors.user_err Pp.(str "notations not supported");
     let name = [Names.Id.to_string name.CAst.v] in
     let constructors =
-          List.map (function (Vernacexpr.(NoCoercion,NoInstance),c) -> c
+          List.map (function (Vernacexpr.(_,NoCoercion,NoInstance),c) -> c
             | _ -> CErrors.user_err Pp.(str "coercion and instance flags not supported"))
             constructors in
     let { template; udecl; cumulative; poly; finite } = flags in