Adapt to coq/coq#18624 (Tac2ffi / Tac2val split)

mit-plv · Feb 6, 2024 · fac98b7 · fac98b7
1 parent f86955b
commit fac98b7
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/Rewriter/Util/plugins/ltac2_extra.ml.v820 b/src/Rewriter/Util/plugins/ltac2_extra.ml.v820
@@ -1,12 +1,13 @@
 open Ltac2_plugin
 open Tac2ffi
+open Tac2val
 open Tac2expr
 open Proofview.Notations
 
 let pname s = { mltac_plugin = "coq-rewriter.ltac2_extra"; mltac_tactic = s }
 
 let define_primitive name arity f =
-  Tac2env.define_primitive (pname name) (Tac2ffi.mk_closure_val arity f)
+  Tac2env.define_primitive (pname name) (Tac2val.mk_closure_val arity f)
 
 let define2 name r0 r1 f = define_primitive name (arity_suc arity_one) begin fun x y ->
   f (Tac2ffi.repr_to r0 x) (Tac2ffi.repr_to r1 y)