Merge pull request #1 from FissoreD/path-stdlib

[TC] prefix of pred name for tc of Classes from Coq/Stdpp...

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' = Hd),
+        std.fold Tl Hd' (x\acc\r\ r is acc ^ "." ^ x) Path', 
         Path is Path' ^ ".tc-"),
     % CAVEAT : Non-ascii caractars can't be part of a pred
     %          name, we replace ö with o

apps/tc/tests/bigTest.v

@@ -882,23 +882,14 @@ instances *)
 Section prod_setoid.
   Context `{Equiv A, Equiv B}.
   Elpi Accumulate TC.Solver lp:{{
-    /* uncomment when requiring Coq >= 8.21
-    shorten tc-Stdlib.Classes.RelationClasses.{tc-Equivalence}. */
-    /* remove below definition when requiring Coq >= 8.21 */
+    shorten tc-.Classes.RelationClasses.{tc-Equivalence}.
     :after "lastHook"
-    tc-Coq.Classes.RelationClasses.tc-Equivalence A RA R :-
+    tc-Equivalence A RA R :-
       RA = {{@equiv _ (@prod_equiv _ _ _ _)}},
       RA' = {{@prod_relation _ _ _ _}},
       coq.unify-eq RA RA' ok,
       % coq.say A RA,
-      tc-Coq.Classes.RelationClasses.tc-Equivalence A RA' R.
-    :after "lastHook"
-    tc-Stdlib.Classes.RelationClasses.tc-Equivalence A RA R :-
-      RA = {{@equiv _ (@prod_equiv _ _ _ _)}},
-      RA' = {{@prod_relation _ _ _ _}},
-      coq.unify-eq RA RA' ok,
-      % coq.say A RA,
-      tc-Stdlib.Classes.RelationClasses.tc-Equivalence A RA' R.
+      tc-Equivalence A RA' R.
   }}.
   (* Elpi Typecheck TC.Solver. *)
 
@@ -919,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-.Classes.Morphisms.{tc-Proper}.
 
     :after "lastHook" 
     tc-Proper A B C R :-
@@ -1052,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-.Classes.Morphisms.{tc-Proper}.
     :after "lastHook" 
     tc-Proper A B C R :-
       B = {{ @respectful _ _ _ _ }},