diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi
index 9062241f9..c228ff7ab 100644
--- a/HB/common/stdpp.elpi
+++ b/HB/common/stdpp.elpi
@@ -101,8 +101,7 @@ constraint print-ctx mixin-src {
 
 % approximation, it should be logical path, not the file name
 pred coq.env.current-library o:string.
-coq.env.current-library L :- coq.version _ _ N _, N >= 13, !,
-  loc.fields {get-option "elpi.loc"} L _ _ _ _.
+coq.env.current-library L :- loc.fields {get-option "elpi.loc"} L _ _ _ _.
 coq.env.current-library "dummy.v".
 
 pred coq.prod-tgt->gref i:term, o:gref.
diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi
index f7c1e76fa..0eb53d2dc 100644
--- a/HB/common/utils.elpi
+++ b/HB/common/utils.elpi
@@ -120,13 +120,6 @@ nice-gref->string X Mod :-
 nice-gref->string X S :-
   coq.term->string (global X) S.
 
-pred compat.concat i:string, i:list string, o:string.
-compat.concat S L O :- coq.version _ _ N _, N > 12, !, std.string.concat S L O.
-compat.concat S L O :- compat.concat.aux L S O.
-compat.concat.aux [] _ "".
-compat.concat.aux [X] _ X :- !.
-compat.concat.aux [X|XS] Sep O :- compat.concat.aux XS Sep O1, O is X ^ Sep ^ O1.
-
 pred gref->modname i:gref, i:int, i:string, o:string.
 gref->modname GR NComp Sep ModName :-
   coq.gref->path GR Path,
@@ -134,7 +127,7 @@ gref->modname GR NComp Sep ModName :-
   std.length Path Len,
   if (Len >= NComp) true (coq.error "Not enough enclosing modules for" {coq.gref->string GR}),
   std.take NComp Mods L,
-  compat.concat Sep {std.rev L} ModName.
+  std.string.concat Sep {std.rev L} ModName.
 pred gref->modname-label i:gref, i:int, i:string, o:string.
 gref->modname-label GR NComp Sep ModName :-
   coq.gref->path GR Path,
@@ -142,7 +135,7 @@ gref->modname-label GR NComp Sep ModName :-
   std.length PathRev Len,
   if (Len >= NComp) (N = NComp) (N = Len),
   std.take N PathRev L,
-  compat.concat Sep {std.rev [{coq.gref->id GR}|L]} ModName.
+  std.string.concat Sep {std.rev [{coq.gref->id GR}|L]} ModName.
 
 pred avoid-name-collision i:string, o:string.
 avoid-name-collision S S1 :-
diff --git a/HB/graph.elpi b/HB/graph.elpi
index 27c7495c3..b8baffcf4 100644
--- a/HB/graph.elpi
+++ b/HB/graph.elpi
@@ -18,13 +18,6 @@ to-file File :- !, std.do! [
 
 namespace private {
 
-pred compat.concat i:string, i:list string, o:string.
-compat.concat S L O :- coq.version _ _ N _, N > 12, !, std.string.concat S L O.
-compat.concat S L O :- compat.concat.aux L S O.
-compat.concat.aux [] _ "".
-compat.concat.aux [X] _ X :- !.
-compat.concat.aux [X|XS] Sep O :- compat.concat.aux XS Sep O1, O is X ^ Sep ^ O1.
-
 pred gref->modname i:gref, i:int, i:string, o:string.
 gref->modname GR NComp Sep ModName :-
   coq.gref->path GR Path,
@@ -32,7 +25,7 @@ gref->modname GR NComp Sep ModName :-
   std.length Path Len,
   if (Len >= NComp) true (coq.error "Not enough enclosing modules for" {coq.gref->string GR}),
   std.take NComp Mods L,
-  compat.concat Sep {std.rev L} ModName.
+  std.string.concat Sep {std.rev L} ModName.
 
 pred pp-coercion-dot i:out_stream, i:coercion. 
 pp-coercion-dot OC (coercion _ _ Src (grefclass Tgt)) :- class-def (class Src _ _), class-def (class Tgt _ _), !, std.do! [
diff --git a/structures.v b/structures.v
index abae6db4b..a6d1c52a9 100644
--- a/structures.v
+++ b/structures.v
@@ -252,8 +252,6 @@ Elpi Accumulate Db hb.db.
 #[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate lp:{{
 
-main _ :- coq.version _ _ N _, N < 13, !,
-  coq.say "HB: HB.locate requires Coq version 8.13 or above".
 main [str S] :- !,
   if (decl-location {coq.locate S} Loc)
      (coq.say "HB: synthesized in file" Loc)