stdlib-inject.patch

From 00a0b0573307a6eb209f267af578087095d1d5c6 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/Classes/SetoidTactics.v | 2 ++
 theories/Init/Notations.v        | 4 ++--
 theories/Init/Tactics.v          | 1 +
 3 files changed, 5 insertions(+), 2 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..e5fc88b7e6 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -126,5 +126,5 @@ Open Scope type_scope.
 (** ML Tactic Notations *)
 
 Declare ML Module "ltac_plugin".
-
-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.36.1