From 43447bca046ca72326e1c7479a4921a0e216a8f8 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 19 Sep 2023 11:26:17 -0700
Subject: [PATCH] `Proj.equal` has been upstreamed, so use it directly (#114)

---
 src/Rewriter/Util/Tactics2/Proj.v.v815 | 2 +-
 src/Rewriter/Util/Tactics2/Proj.v.v816 | 9 ++++++++-
 src/Rewriter/Util/Tactics2/Proj.v.v818 | 5 +----
 src/Rewriter/Util/Tactics2/Proj.v.v819 | 5 +----
 4 files changed, 11 insertions(+), 10 deletions(-)
 mode change 120000 => 100644 src/Rewriter/Util/Tactics2/Proj.v.v816

diff --git a/src/Rewriter/Util/Tactics2/Proj.v.v815 b/src/Rewriter/Util/Tactics2/Proj.v.v815
index 465195d00..fef9a05f6 120000
--- a/src/Rewriter/Util/Tactics2/Proj.v.v815
+++ b/src/Rewriter/Util/Tactics2/Proj.v.v815
@@ -1 +1 @@
-Proj.v.v818
\ No newline at end of file
+Proj.v.v816
\ No newline at end of file
diff --git a/src/Rewriter/Util/Tactics2/Proj.v.v816 b/src/Rewriter/Util/Tactics2/Proj.v.v816
deleted file mode 120000
index 465195d00..000000000
--- a/src/Rewriter/Util/Tactics2/Proj.v.v816
+++ /dev/null
@@ -1 +0,0 @@
-Proj.v.v818
\ No newline at end of file
diff --git a/src/Rewriter/Util/Tactics2/Proj.v.v816 b/src/Rewriter/Util/Tactics2/Proj.v.v816
new file mode 100644
index 000000000..6c0e12e9c
--- /dev/null
+++ b/src/Rewriter/Util/Tactics2/Proj.v.v816
@@ -0,0 +1,8 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.
+Import Constr.Unsafe.
+
+Ltac2 equal (x : projection) (y : projection) : bool
+  := let dummy := make (Rel (-1)) in
+     Constr.equal (make (Proj x dummy)) (make (Proj y dummy)).
diff --git a/src/Rewriter/Util/Tactics2/Proj.v.v818 b/src/Rewriter/Util/Tactics2/Proj.v.v818
index 6c0e12e9c..2715b7a21 100644
--- a/src/Rewriter/Util/Tactics2/Proj.v.v818
+++ b/src/Rewriter/Util/Tactics2/Proj.v.v818
@@ -1,8 +1,5 @@
 Require Import Ltac2.Ltac2.
+Require Export Ltac2.Proj.
 Require Export Rewriter.Util.FixCoqMistakes.
 Import Ltac2.Constr.
 Import Constr.Unsafe.
-
-Ltac2 equal (x : projection) (y : projection) : bool
-  := let dummy := make (Rel (-1)) in
-     Constr.equal (make (Proj x dummy)) (make (Proj y dummy)).
diff --git a/src/Rewriter/Util/Tactics2/Proj.v.v819 b/src/Rewriter/Util/Tactics2/Proj.v.v819
index 6c0e12e9c..2715b7a21 100644
--- a/src/Rewriter/Util/Tactics2/Proj.v.v819
+++ b/src/Rewriter/Util/Tactics2/Proj.v.v819
@@ -1,8 +1,5 @@
 Require Import Ltac2.Ltac2.
+Require Export Ltac2.Proj.
 Require Export Rewriter.Util.FixCoqMistakes.
 Import Ltac2.Constr.
 Import Constr.Unsafe.
-
-Ltac2 equal (x : projection) (y : projection) : bool
-  := let dummy := make (Rel (-1)) in
-     Constr.equal (make (Proj x dummy)) (make (Proj y dummy)).