Adapt to coq/coq#19310

LPCIC · Jul 15, 2024 · a62a92c · a62a92c
1 parent c13ecc9
commit a62a92c
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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 _ _ _ _ }},