diff --git a/.gitignore b/.gitignore
index 7ada95cf1..804803d82 100644
--- a/.gitignore
+++ b/.gitignore
@@ -94,6 +94,7 @@ src/Rewriter/Util/plugins/definition_by_tactic_plugin.ml
 src/Rewriter/Util/plugins/inductive_from_elim_plugin.ml
 src/Rewriter/Util/plugins/rewriter_build_plugin.ml
 src/Rewriter/Util/plugins/strategy_tactic_plugin.ml
+src/Rewriter/Util/plugins/ltac2_extra_plugin.ml
 
 src/Rewriter/Util/plugins/RewriterBuildRegistry.v
 src/Rewriter/Util/plugins/RewriterBuild.v
@@ -114,6 +115,10 @@ src/Rewriter/Util/plugins/strategy_tactic.ml
 src/Rewriter/Util/plugins/strategy_tactic.mli
 src/Rewriter/Util/plugins/strategy_tactic_plugin.mlg
 src/Rewriter/Util/plugins/strategy_tactic_plugin.mllib
+src/Rewriter/Util/plugins/ltac2_extra.ml
+src/Rewriter/Util/plugins/ltac2_extra.mli
+src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg
+src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib
 
 /.coq-version
 /.coq-version-compilation-date
diff --git a/Makefile.local-late b/Makefile.local-late
index 0f700c06e..a3c190a25 100644
--- a/Makefile.local-late
+++ b/Makefile.local-late
@@ -15,3 +15,6 @@ OTHERFLAGS += -w -notation-overridden
 ifneq ($(PROFILE),)
 OTHERFLAGS += -profile-ltac
 endif
+
+# Kludge around COQBUG(https://github.com/coq/coq/issues/16591)
+FINDLIBPKGS += -package coq-core.plugins.ltac2
diff --git a/Makefile.local.common b/Makefile.local.common
index c373c56ff..713a49b9d 100644
--- a/Makefile.local.common
+++ b/Makefile.local.common
@@ -45,7 +45,12 @@ COMPATIBILITY_FILES := \
 	src/Rewriter/Util/plugins/strategy_tactic.mli \
 	src/Rewriter/Util/plugins/strategy_tactic_plugin.mlg \
 	src/Rewriter/Util/plugins/strategy_tactic_plugin.mllib \
+	src/Rewriter/Util/plugins/ltac2_extra.ml \
+	src/Rewriter/Util/plugins/ltac2_extra.mli \
+	src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg \
+	src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib \
 	src/Rewriter/Util/plugins/RewriterBuildRegistry.v \
 	src/Rewriter/Util/plugins/RewriterBuild.v \
 	src/Rewriter/Util/plugins/StrategyTactic.v \
+	src/Rewriter/Util/plugins/Ltac2Extra.v \
 	#
diff --git a/_CoqProject.in b/_CoqProject.in
index 6b3e5c926..9bb66f744 100644
--- a/_CoqProject.in
+++ b/_CoqProject.in
@@ -141,6 +141,12 @@ src/Rewriter/Util/plugins/strategy_tactic.ml
 src/Rewriter/Util/plugins/strategy_tactic.mli
 src/Rewriter/Util/plugins/strategy_tactic_plugin.mlg
 src/Rewriter/Util/plugins/strategy_tactic_plugin.mllib
+src/Rewriter/Util/plugins/ltac2_extra.ml
+src/Rewriter/Util/plugins/ltac2_extra.mli
+src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg
+src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib
 src/Rewriter/Util/plugins/RewriterBuildRegistry.v
-src/Rewriter/Util/plugins/StrategyTactic.v
 src/Rewriter/Util/plugins/RewriterBuild.v
+src/Rewriter/Util/plugins/StrategyTactic.v
+src/Rewriter/Util/plugins/Ltac2Extra.v
+
diff --git a/src/Rewriter/Util/plugins/Ltac2Extra.v.v815 b/src/Rewriter/Util/plugins/Ltac2Extra.v.v815
new file mode 100644
index 000000000..7f53e77f7
--- /dev/null
+++ b/src/Rewriter/Util/plugins/Ltac2Extra.v.v815
@@ -0,0 +1,10 @@
+Require Import Ltac2.Ltac2.
+
+Declare ML Module "ltac2_extra_plugin".
+
+Module Ltac2.
+  Module Constr.
+    Export Ltac2.Constr.
+    Ltac2 @ external equal_nounivs : constr -> constr -> bool := "ltac2" "constr_equal_nounivs".
+  End Constr.
+End Ltac2.
diff --git a/src/Rewriter/Util/plugins/Ltac2Extra.v.v816 b/src/Rewriter/Util/plugins/Ltac2Extra.v.v816
new file mode 100644
index 000000000..176c46e06
--- /dev/null
+++ b/src/Rewriter/Util/plugins/Ltac2Extra.v.v816
@@ -0,0 +1,10 @@
+Require Import Ltac2.Ltac2.
+
+Declare ML Module "coq-rewriter.ltac2_extra".
+
+Module Ltac2.
+  Module Constr.
+    Export Ltac2.Constr.
+    Ltac2 @ external equal_nounivs : constr -> constr -> bool := "ltac2" "constr_equal_nounivs".
+  End Constr.
+End Ltac2.
diff --git a/src/Rewriter/Util/plugins/Ltac2Extra.v.v817 b/src/Rewriter/Util/plugins/Ltac2Extra.v.v817
new file mode 100644
index 000000000..176c46e06
--- /dev/null
+++ b/src/Rewriter/Util/plugins/Ltac2Extra.v.v817
@@ -0,0 +1,10 @@
+Require Import Ltac2.Ltac2.
+
+Declare ML Module "coq-rewriter.ltac2_extra".
+
+Module Ltac2.
+  Module Constr.
+    Export Ltac2.Constr.
+    Ltac2 @ external equal_nounivs : constr -> constr -> bool := "ltac2" "constr_equal_nounivs".
+  End Constr.
+End Ltac2.
diff --git a/src/Rewriter/Util/plugins/META.coq-rewriter b/src/Rewriter/Util/plugins/META.coq-rewriter
index ffcaadc4e..2b5a84d8e 100644
--- a/src/Rewriter/Util/plugins/META.coq-rewriter
+++ b/src/Rewriter/Util/plugins/META.coq-rewriter
@@ -34,4 +34,13 @@ package "rewriter_build" (
   plugin(byte) = "rewriter_build_plugin.cma"
   plugin(native) = "rewriter_build_plugin.cmxs"
 )
+package "ltac2_extra" (
+  directory = "."
+  description = "Coq Ltac2 Extra Tactics"
+  requires = "coq-core.plugins.ltac2"
+  archive(byte) = "ltac2_extra_plugin.cma"
+  archive(native) = "ltac2_extra_plugin.cmxa"
+  plugin(byte) = "ltac2_extra_plugin.cma"
+  plugin(native) = "ltac2_extra_plugin.cmxs"
+)
 directory = "."
diff --git a/src/Rewriter/Util/plugins/ltac2_extra.ml.v815 b/src/Rewriter/Util/plugins/ltac2_extra.ml.v815
new file mode 100644
index 000000000..a8843adfc
--- /dev/null
+++ b/src/Rewriter/Util/plugins/ltac2_extra.ml.v815
@@ -0,0 +1,19 @@
+open Ltac2_plugin
+open Tac2ffi
+open Tac2expr
+open Proofview.Notations
+
+let pname s = { mltac_plugin = "coq-core.plugins.ltac2"; mltac_tactic = s }
+
+let define_primitive name arity f =
+  Tac2env.define_primitive (pname name) (Tac2ffi.mk_closure 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)
+end
+
+let () = define2 "constr_equal_nounivs" constr constr begin fun c1 c2 ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let b = EConstr.eq_constr_nounivs sigma c1 c2 in
+  Proofview.tclUNIT (Tac2ffi.of_bool b)
+end
diff --git a/src/Rewriter/Util/plugins/ltac2_extra.ml.v816 b/src/Rewriter/Util/plugins/ltac2_extra.ml.v816
new file mode 100644
index 000000000..a8843adfc
--- /dev/null
+++ b/src/Rewriter/Util/plugins/ltac2_extra.ml.v816
@@ -0,0 +1,19 @@
+open Ltac2_plugin
+open Tac2ffi
+open Tac2expr
+open Proofview.Notations
+
+let pname s = { mltac_plugin = "coq-core.plugins.ltac2"; mltac_tactic = s }
+
+let define_primitive name arity f =
+  Tac2env.define_primitive (pname name) (Tac2ffi.mk_closure 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)
+end
+
+let () = define2 "constr_equal_nounivs" constr constr begin fun c1 c2 ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let b = EConstr.eq_constr_nounivs sigma c1 c2 in
+  Proofview.tclUNIT (Tac2ffi.of_bool b)
+end
diff --git a/src/Rewriter/Util/plugins/ltac2_extra.ml.v817 b/src/Rewriter/Util/plugins/ltac2_extra.ml.v817
new file mode 100644
index 000000000..a8843adfc
--- /dev/null
+++ b/src/Rewriter/Util/plugins/ltac2_extra.ml.v817
@@ -0,0 +1,19 @@
+open Ltac2_plugin
+open Tac2ffi
+open Tac2expr
+open Proofview.Notations
+
+let pname s = { mltac_plugin = "coq-core.plugins.ltac2"; mltac_tactic = s }
+
+let define_primitive name arity f =
+  Tac2env.define_primitive (pname name) (Tac2ffi.mk_closure 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)
+end
+
+let () = define2 "constr_equal_nounivs" constr constr begin fun c1 c2 ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let b = EConstr.eq_constr_nounivs sigma c1 c2 in
+  Proofview.tclUNIT (Tac2ffi.of_bool b)
+end
diff --git a/src/Rewriter/Util/plugins/ltac2_extra.mli.v815 b/src/Rewriter/Util/plugins/ltac2_extra.mli.v815
new file mode 100644
index 000000000..e69de29bb
diff --git a/src/Rewriter/Util/plugins/ltac2_extra.mli.v816 b/src/Rewriter/Util/plugins/ltac2_extra.mli.v816
new file mode 100644
index 000000000..e69de29bb
diff --git a/src/Rewriter/Util/plugins/ltac2_extra.mli.v817 b/src/Rewriter/Util/plugins/ltac2_extra.mli.v817
new file mode 100644
index 000000000..e69de29bb
diff --git a/src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg.v815 b/src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg.v815
new file mode 100644
index 000000000..caffbc0a6
--- /dev/null
+++ b/src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg.v815
@@ -0,0 +1 @@
+DECLARE PLUGIN "coq-rewriter.ltac2_extra"
diff --git a/src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg.v816 b/src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg.v816
new file mode 100644
index 000000000..caffbc0a6
--- /dev/null
+++ b/src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg.v816
@@ -0,0 +1 @@
+DECLARE PLUGIN "coq-rewriter.ltac2_extra"
diff --git a/src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg.v817 b/src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg.v817
new file mode 100644
index 000000000..caffbc0a6
--- /dev/null
+++ b/src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg.v817
@@ -0,0 +1 @@
+DECLARE PLUGIN "coq-rewriter.ltac2_extra"
diff --git a/src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib.v815 b/src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib.v815
new file mode 100644
index 000000000..c1effb855
--- /dev/null
+++ b/src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib.v815
@@ -0,0 +1,2 @@
+Ltac2_extra
+Ltac2_extra_plugin
diff --git a/src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib.v816 b/src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib.v816
new file mode 100644
index 000000000..c1effb855
--- /dev/null
+++ b/src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib.v816
@@ -0,0 +1,2 @@
+Ltac2_extra
+Ltac2_extra_plugin
diff --git a/src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib.v817 b/src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib.v817
new file mode 100644
index 000000000..c1effb855
--- /dev/null
+++ b/src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib.v817
@@ -0,0 +1,2 @@
+Ltac2_extra
+Ltac2_extra_plugin