From 6124e37ca43345969b6e158265eef7c13dec1e01 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Sat, 13 Jul 2024 11:52:38 +0200
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19310

---
 apps/coercion/tests/coercion.t/test.v      | 1 +
 apps/coercion/tests/coercion_open.t/test.v | 1 +
 apps/tc/elpi/tc_aux.elpi                   | 3 ++-
 apps/tc/tests/bigTest.v                    | 6 +++---
 4 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/apps/coercion/tests/coercion.t/test.v b/apps/coercion/tests/coercion.t/test.v
index 932605cb2..de11d41db 100644
--- a/apps/coercion/tests/coercion.t/test.v
+++ b/apps/coercion/tests/coercion.t/test.v
@@ -1,4 +1,5 @@
 From elpi.apps Require Import coercion.
+#[warning="-deprecated-from-Coq"]
 From Coq Require Import Bool.
 
 Elpi Accumulate coercion.db lp:{{
diff --git a/apps/coercion/tests/coercion_open.t/test.v b/apps/coercion/tests/coercion_open.t/test.v
index c4d533305..56dd6e8f9 100644
--- a/apps/coercion/tests/coercion_open.t/test.v
+++ b/apps/coercion/tests/coercion_open.t/test.v
@@ -1,4 +1,5 @@
 From elpi.apps Require Import coercion.
+#[warning="-deprecated-from-Coq"]
 From Coq Require Import Arith ssreflect.
 
 Ltac my_solver := trivial with arith.
diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
index 1ec0e63e6..a6f7fd352 100644
--- a/apps/tc/elpi/tc_aux.elpi
+++ b/apps/tc/elpi/tc_aux.elpi
@@ -93,7 +93,8 @@ namespace tc {
     if (tc.is-option-active tc.oTC-clauseNameShortName)
       (Path = "")
       (coq.gref->path Gr [Hd | Tl], 
-        std.fold Tl Hd (x\acc\r\ r is acc ^ "." ^ x) Path', 
+        if (Hd = "Coq") (Hd' = "Stdlib") (Hd' = Hd),
+        std.string.concat "." [Hd'|Tl] Path',
         Path is Path' ^ ".tc-"),
     % CAVEAT : Non-ascii caractars can't be part of a pred
     %          name, we replace ö with o
diff --git a/apps/tc/tests/bigTest.v b/apps/tc/tests/bigTest.v
index 8368d44c0..52d8bd617 100644
--- a/apps/tc/tests/bigTest.v
+++ b/apps/tc/tests/bigTest.v
@@ -882,7 +882,7 @@ instances *)
 Section prod_setoid.
   Context `{Equiv A, Equiv B}.
   Elpi Accumulate TC.Solver lp:{{
-    shorten tc-Coq.Classes.RelationClasses.{tc-Equivalence}.
+    shorten tc-Stdlib.Classes.RelationClasses.{tc-Equivalence}.
     :after "lastHook"
     tc-Equivalence A RA R :-
       RA = {{@equiv _ (@prod_equiv _ _ _ _)}},
@@ -910,7 +910,7 @@ Section prod_setoid.
       std.map L1 remove_equiv_prod_equiv L2.
     remove_equiv_prod_equiv A A.
 
-    shorten tc-Coq.Classes.Morphisms.{tc-Proper}.
+    shorten tc-Stdlib.Classes.Morphisms.{tc-Proper}.
     
     :after "lastHook" 
     tc-Proper A B C R :-
@@ -1043,7 +1043,7 @@ Elpi Accumulate TC.Solver lp:{{
       std.map L1 remove_equiv_sum_equiv L2.
     remove_equiv_sum_equiv A A.
     
-    shorten tc-Coq.Classes.Morphisms.{tc-Proper}.
+    shorten tc-Stdlib.Classes.Morphisms.{tc-Proper}.
     :after "lastHook" 
     tc-Proper A B C R :-
       B = {{ @respectful _ _ _ _ }},