Compat typeclass for list_reifyl

SkySkimmer · Nov 21, 2023 · 3b1b653 · 3b1b653
1 parent ea815c1
commit 3b1b653
Showing 1 changed file with 5 additions and 0 deletions.
diff --git 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 :=