Proj.equal has been upstreamed, so use it directly (#114)

mit-plv · Sep 19, 2023 · 43447bc · 43447bc
1 parent 42b34e5
commit 43447bc
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 10 deletions.
diff --git a/src/Rewriter/Util/Tactics2/Proj.v.v815 b/src/Rewriter/Util/Tactics2/Proj.v.v815
@@ -1 +1 @@
-Proj.v.v818
+Proj.v.v816
diff --git a/src/Rewriter/Util/Tactics2/Proj.v.v816 b/src/Rewriter/Util/Tactics2/Proj.v.v816
diff --git a/src/Rewriter/Util/Tactics2/Proj.v.v816 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
@@ -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
@@ -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)).