Skip to content

Commit 0cfb58b

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

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
@@ -458,8 +458,8 @@ Elpi Export HB.end.
458458
(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
459459
(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
460460

461-
(** [HB.exports] rexports Exports modules that have been accumulated by
462-
[HB.structure] (it contains canonical, coercions and ELPI metadata) *)
461+
(** [HB.export Modname] does the work of [Export Modname] but also schedules [Modname]
462+
to be exported later on, when [HB.reexport] is called. *)
463463

464464
Elpi Command HB.export.
465465
Elpi Accumulate File "hb.elpi".

0 commit comments

Comments
 (0)