Remove outdated Coq version tests now that we require 8.15

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.

HB/common/utils.elpi

@@ -120,29 +120,22 @@ 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,
   std.rev Path Mods,
   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,
   std.rev Path PathRev,
   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 :-

HB/graph.elpi

@@ -18,21 +18,14 @@ 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,
   std.rev Path Mods,
   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! [

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)