From a5617debac5115e8f152cf5afa8df5235a80a988 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Thu, 16 Nov 2023 09:53:41 +0100
Subject: [PATCH] Compat typeclass for list_reifyl

---
 theories/setoid_ring/Ncring_tac.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/setoid_ring/Ncring_tac.v b/theories/setoid_ring/Ncring_tac.v
index 106fe75fe1863..11259a81102f1 100644
--- a/theories/setoid_ring/Ncring_tac.v
+++ b/theories/setoid_ring/Ncring_tac.v
@@ -130,6 +130,11 @@ Ltac list_reifyl0 lterm :=
       list_reifyl lvar lterm
   end.
 
+Class ReifyL {R:Type} (lvar lterm : list R) := list_reifyl : (list R * list (PExpr Z)).
+Arguments list_reifyl {R lvar lterm}.
+
+Global Hint Extern 0 (ReifyL lvar lterm) => let reif := list_reifyl lvar lterm in exact reif : typeclass_instances.
+
 Unset Implicit Arguments.
 
 Ltac lterm_goal g :=