Syntax errors on `Require Import` after HB is imported.

[arthuraa]

If I have a Rocq project with a lib file, I cannot import that file after I import HB. For concreteness, suppose that I have a project consisting of

(* lib.v *)
Definition n := 42.

and

(* foo.v *)
From HB Require Import structures.
Require Import lib.

After I compile lib and try to compile foo, I get the following error:

Error: Syntax error: [filtered_import] expected after [export_token] (in [gallina_ext]).

If I swap the two imports, then the file compiles fine. If I replace lib with library, then the syntax error goes away (and Rocq complains about the missing vo file instead).

[CohenCyril]

I suspect this is elpi rather than HB. I'll check with a computer.