Skip to content

Commit f6fd7ec

Browse files
garesCohenCyril
authored andcommitted
note about attribute parsing hack
1 parent f88a2bc commit f6fd7ec

File tree

1 file changed

+4
-2
lines changed

1 file changed

+4
-2
lines changed

hb.elpi

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -83,21 +83,23 @@ under.do! Then LP :- Then (_\ std.do! LP) _.
8383
%%%%% HB Utils %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
8484

8585

86-
% HACK: move to coq-elpi proper
86+
% HACK: move to coq-elpi proper, remove when coq-elpi > 1.9.2
8787
type attmap attribute-type.
8888

8989
% runs P in a context where Coq #[attributes] are parsed
9090
pred with-attributes i:prop.
9191
with-attributes P :-
9292
attributes A,
93-
% HACK: move to coq-elpi proper
93+
94+
% HACK: move to coq-elpi proper, remove when coq-elpi > 1.9.2
9495
(pi S L AS Prefix R R1 Map PS\
9596
parse-attributes.aux [attribute S (node L)|AS] Prefix R :-
9697
if (Prefix = "") (PS = S) (PS is Prefix ^ "." ^ S), supported-attribute (att PS attmap), !,
9798
parse-attributes.aux AS Prefix R1,
9899
(pi x\ supported-attribute (att x string) :- !) => parse-attributes.aux L "" Map,
99100
std.append R1 [get-option PS Map] R
100101
) =>
102+
101103
coq.parse-attributes A [
102104
att "verbose" bool,
103105
att "mathcomp" bool,

0 commit comments

Comments
 (0)