Adapt to coq/coq#17475 (Ltac2 externals can have arity 0) (#102)

mit-plv · May 2, 2023 · 3065375 · 3065375
1 parent f532c8b
commit 3065375
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Rewriter/Util/plugins/ltac2_extra.ml.v818 b/src/Rewriter/Util/plugins/ltac2_extra.ml.v818
@@ -6,7 +6,7 @@ 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 arity f)
+  Tac2env.define_primitive (pname name) (Tac2ffi.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)