Add external Ltac2.Constr.equal_nounivs

We'll connect it up after doing a performance measurement

.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

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

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 \
 	#

_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
+

src/Rewriter/Util/plugins/Ltac2Extra.v.v815

@@ -0,0 +1,10 @@
+Require Import Ltac2.Ltac2.
+
+Declare ML Module "ltac2_extra".
+
+Module Ltac2.
+  Module Constr.
+    Export Ltac2.Constr.
+    Ltac2 @ external equal_nounivs : constr -> constr -> bool := "ltac2" "constr_equal_nounivs".
+  End Constr.
+End Ltac2.

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.

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.

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 = "."

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

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

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

src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg.v815

@@ -0,0 +1 @@
+DECLARE PLUGIN "coq-rewriter.ltac2_extra"

src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg.v816

@@ -0,0 +1 @@
+DECLARE PLUGIN "coq-rewriter.ltac2_extra"

src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg.v817

@@ -0,0 +1 @@
+DECLARE PLUGIN "coq-rewriter.ltac2_extra"

src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib.v815

@@ -0,0 +1,2 @@
+Ltac2_extra
+Ltac2_extra_plugin

src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib.v816

@@ -0,0 +1,2 @@
+Ltac2_extra
+Ltac2_extra_plugin

src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib.v817

@@ -0,0 +1,2 @@
+Ltac2_extra
+Ltac2_extra_plugin