diff options
Diffstat (limited to 'intf/vernacexpr.mli')
| -rw-r--r-- | intf/vernacexpr.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 5bf83e2c1..b784bc433 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -223,6 +223,8 @@ type section_subset_expr = type section_subset_descr = SsAll | SsType | SsExpr of section_subset_expr +type extend_name = string * int + (* This type allows registering the inlining of constants in native compiler. It will be extended with primitive inductive types and operators *) type register_kind = @@ -427,7 +429,7 @@ type vernac_expr = | VernacToplevelControl of exn (* For extension *) - | VernacExtend of string * Genarg.raw_generic_argument list + | VernacExtend of extend_name * Genarg.raw_generic_argument list (* Flags *) | VernacProgram of vernac_expr |