diff options
Diffstat (limited to 'intf/vernacexpr.mli')
| -rw-r--r-- | intf/vernacexpr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index ee3a0dcf1..238eeb82e 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -224,7 +224,7 @@ type section_subset_expr = type section_subset_descr = SsAll | SsType | SsExpr of section_subset_expr -(* This type allows to register inline of constants in native compiler. +(* This type allows registering the inlining of constants in native compiler. It will be extended with primitive inductive types and operators *) type register_kind = | RegisterInline |