From 08bdf4eb3e73c8201148bed35605310cd35003e8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tom=C3=A1s=20D=C3=ADaz?= <tomdtron@gmail.com>
Date: Fri, 9 Jan 2026 15:03:18 +0100
Subject: [PATCH] Adapt to rocq-prover/rocq#21438 (Check for existing relevant
 field)

---
 src/lean.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/lean.ml b/src/lean.ml
index c07dafd..985f9ac 100644
--- a/src/lean.ml
+++ b/src/lean.ml
@@ -1306,7 +1306,14 @@ and declare_ind { name = n; params; ty; ctors; univs } i =
                  match (fields, Sorts.is_sprop sort) with
                  | [], true -> (None, [], ctys)
                  | _ :: _, false ->
-                   (Some (Some [| default_proj_id |]), fields, [ cty' ])
+                   if
+                     List.exists
+                       (fun (na, _) ->
+                         na.Context.binder_relevance
+                         == EConstr.ERelevance.relevant)
+                       fields
+                   then (Some (Some [| default_proj_id |]), fields, [ cty' ])
+                   else (None, [], ctys)
                  | [], false -> (None, [], ctys)
                  | _ :: _, true ->
                    if