Elpi reports duplicate macro definitions across different files.

[maggesi]

Consider a file file1.elpi that defines a macro:

macro @a :- tt.
pred test1 o:bool.
test1 @a.

The scope of the macro do not extend beyond file1.elpi as it can be seen in this example file2.elpi:

accumulate file1.
pred test2 o:bool.
test2 @a.

goal> test2 A.
Fatal error: file2.elpi, characters 38-47, line 4, column 4: Undeclared macro @a

However, if one try to redefine the macro in another file, Elpi report it as a duplicate declaration. E.g., file3.elpi:

accumulate file1.
macro @a :- tt.
pred test3 o:bool.
test3 @a.

goal> test3 A.
Fatal error: file1.elpi, characters 0-15, line 1, column 10: Macro @a declared twice:
first declaration: file3.elpi, characters 19-34, line 3, column 10
second declaration: file1.elpi, characters 0-15, line 1, column 10