hack: backport from coq-elpi a new kind of attribute (map)

in this way we can parse #[infer(P = "foo", Q = "bar")]

Author: gares

hb.elpi

@@ -82,17 +82,31 @@ under.do! Then LP :- Then (_\ std.do! LP) _.
 
 %%%%% HB Utils %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+
+% HACK: move to coq-elpi proper
+type attmap attribute-type.
+
 % runs P in a context where Coq #[attributes] are parsed
 pred with-attributes i:prop.
 with-attributes P :-
   attributes A,
+% HACK: move to coq-elpi proper
+(pi S L AS Prefix R R1 Map PS\ 
+  parse-attributes.aux [attribute S (node L)|AS] Prefix R :-
+    if (Prefix = "") (PS = S) (PS is Prefix ^ "." ^ S), supported-attribute (att PS attmap), !,
+    parse-attributes.aux AS Prefix R1,
+    (pi x\ supported-attribute (att x string) :- !) => parse-attributes.aux L "" Map,
+    std.append R1 [get-option PS Map] R
+) =>
   coq.parse-attributes A [
     att "verbose" bool,
     att "mathcomp" bool,
     att "mathcomp.axiom" string,
+    att "infer" attmap,
   ] Opts, !,
   Opts => P.
 
+
 pred if-verbose i:prop.
 if-verbose P :- get-option "verbose" tt, !, P.
 if-verbose _.