Skip to content

Commit debb007

Browse files
authored
Update structures.v
1 parent 0cfb58b commit debb007

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

structures.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -475,8 +475,8 @@ Elpi Export HB.export.
475475
(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
476476
(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
477477

478-
(** [HB.exports] rexports Exports modules that have been accumulated by
479-
[HB.structure] (it contains canonical, coercions and ELPI metadata) *)
478+
(** [HB.reexport] Exports all modules that were previously exported via [HB.export].
479+
It is useful to create one big module with all exports at the end of a file. *)
480480

481481
Elpi Command HB.reexport.
482482
Elpi Accumulate File "hb.elpi".

0 commit comments

Comments
 (0)