Skip to content

Commit df359be

Browse files
authored
Update structures.v
1 parent debb007 commit df359be

File tree

1 file changed

+12
-1
lines changed

1 file changed

+12
-1
lines changed

structures.v

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -459,7 +459,18 @@ Elpi Export HB.end.
459459
(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
460460

461461
(** [HB.export Modname] does the work of [Export Modname] but also schedules [Modname]
462-
to be exported later on, when [HB.reexport] is called. *)
462+
to be exported later on, when [HB.reexport] is called.
463+
Note that the list of modules to be exported is store in the current module,
464+
hence the recommended way to do is
465+
<<<
466+
Module Algebra.
467+
HB.mixin .... HB.structure ...
468+
Module MoreExports. ... End MoreExports. HB.export MoreExports.
469+
...
470+
Module Export. HB.reexport. End Exports.
471+
End Algebra.
472+
Export Algebra.Exports.
473+
>>> *)
463474

464475
Elpi Command HB.export.
465476
Elpi Accumulate File "hb.elpi".

0 commit comments

Comments
 (0)