From 03296912ffa46037f66abd203995d414f4cdf16c Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Mon, 24 Jan 2022 15:31:41 +0100
Subject: [PATCH 1/2] Add some decomposition directives to the patch

---
 Makefile            |  5 +++++
 stdlib-inject.patch | 40 +++++++++++++++++++++++++++++++++++++---
 2 files changed, 42 insertions(+), 3 deletions(-)

diff --git a/Makefile b/Makefile
index 9d33ffd..7523dcf 100644
--- a/Makefile
+++ b/Makefile
@@ -83,6 +83,11 @@ theories/Init/%.v:
 	@mkdir -p $(dir $@)
 	@cp $(COQLIB)$@ $@
 
+theories/Classes/SetoidTactics.v:
+	@echo "Linking $@"
+	@mkdir -p $(dir $@)
+	@cp $(COQLIB)$@ $@
+
 %.v %.cmxs:
 	@echo "Linking $@"
 	@mkdir -p $(dir $@)
diff --git a/stdlib-inject.patch b/stdlib-inject.patch
index f1b880a..5108e7c 100644
--- a/stdlib-inject.patch
+++ b/stdlib-inject.patch
@@ -1,12 +1,34 @@
-From efc6af59b5e4edaf3e98072ad8a46b23c1da1559 Mon Sep 17 00:00:00 2001
+From 0c375495ac05f09a13037ba07bd5ce63d45d8dba Mon Sep 17 00:00:00 2001
 From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
 Date: Wed, 10 Nov 2021 21:45:29 +0100
 Subject: [PATCH] Patch to inject Tactician into the standard library
 
 ---
- theories/Init/Notations.v | 5 ++---
- 1 file changed, 2 insertions(+), 3 deletions(-)
+ theories/Classes/SetoidTactics.v | 2 ++
+ theories/Init/Notations.v        | 5 ++---
+ theories/Init/Tactics.v          | 1 +
+ 3 files changed, 5 insertions(+), 3 deletions(-)
 
+diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
+index 559a404ddd..82fda2491b 100644
+--- a/theories/Classes/SetoidTactics.v
++++ b/theories/Classes/SetoidTactics.v
+@@ -64,6 +64,7 @@ Ltac setoidreplaceat H t occs :=
+ 
+ Tactic Notation "setoid_replace" constr(x) "with" constr(y) :=
+   setoidreplace (default_relation x y) idtac.
++Tactician Register Tactic "setoid_replace_with" setoid_replace _ with _.
+ 
+ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+   "at" int_or_var_list(o) :=
+@@ -81,6 +82,7 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+   "by" tactic3(t) :=
+   setoidreplace (default_relation x y) ltac:(t).
++Tactician Register Tactic "setoid_replace_with_by" setoid_replace _ with _ by idtac.
+ 
+ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+   "at" int_or_var_list(o)
 diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
 index 77236f77df..7c56963295 100644
 --- a/theories/Init/Notations.v
@@ -20,6 +42,18 @@ index 77236f77df..7c56963295 100644
 -Global Set Default Proof Mode "Classic".
 +From Tactician Require Export Ltac1.Record.
 +Global Set Default Proof Mode "Tactician Ltac1".
+diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
+index db36d0cda7..26fdc9c4a8 100644
+--- a/theories/Init/Tactics.v
++++ b/theories/Init/Tactics.v
+@@ -186,6 +186,7 @@ Ltac easy :=
+   fail "Cannot solve this goal".
+ 
+ Tactic Notation "now" tactic(t) := t; easy.
++Tactician Alias Record (now idtac) Decompose.
+ 
+ (** Slightly more than [easy]*)
+ 
 -- 
 2.34.0
 

From 149d1987f3f958714b5fd1e958e901b193a15c6a Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Tue, 3 May 2022 14:10:30 +0200
Subject: [PATCH 2/2] Load Ltac.Record instead of Require

This will make sure that tactics like reflexivity still have the correct name
like
Coq.Notations.reflexivity instead of Tactician.Ltac.Record.reflexivity.
---
 stdlib-inject.patch | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/stdlib-inject.patch b/stdlib-inject.patch
index 5108e7c..6759b15 100644
--- a/stdlib-inject.patch
+++ b/stdlib-inject.patch
@@ -1,4 +1,4 @@
-From 0c375495ac05f09a13037ba07bd5ce63d45d8dba Mon Sep 17 00:00:00 2001
+From 5715fee7767de5eb197b62947032e91a21a5d529 Mon Sep 17 00:00:00 2001
 From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
 Date: Wed, 10 Nov 2021 21:45:29 +0100
 Subject: [PATCH] Patch to inject Tactician into the standard library
@@ -30,7 +30,7 @@ index 559a404ddd..82fda2491b 100644
  Tactic Notation "setoid_replace" constr(x) "with" constr(y)
    "at" int_or_var_list(o)
 diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
-index 77236f77df..7c56963295 100644
+index 77236f77df..4a3991bde8 100644
 --- a/theories/Init/Notations.v
 +++ b/theories/Init/Notations.v
 @@ -125,6 +125,5 @@ Open Scope type_scope.
@@ -40,7 +40,7 @@ index 77236f77df..7c56963295 100644
 -Declare ML Module "ltac_plugin".
 -
 -Global Set Default Proof Mode "Classic".
-+From Tactician Require Export Ltac1.Record.
++Load "Ltac1/Record".
 +Global Set Default Proof Mode "Tactician Ltac1".
 diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
 index db36d0cda7..26fdc9c4a8 100644
@@ -55,5 +55,5 @@ index db36d0cda7..26fdc9c4a8 100644
  (** Slightly more than [easy]*)
  
 -- 
-2.34.0
+2.36.0