diff --git a/theories/setoid_ring/Ncring_tac.v b/theories/setoid_ring/Ncring_tac.v
index 106fe75fe1863..608b02207936e 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 :=