diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-09 22:13:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-10 00:16:20 +0200 |
| commit | edfa5e986a25eb7a0719d20b43a618cb5bd4cd95 (patch) | |
| tree | e7af11e344a99b2496d22d2bc100f493bd701b96 /intf | |
| parent | 0dd3f0d34873dcd126be8ec48724a310214f38ac (diff) | |
VernacExtend does not dispatch on type anymore.
Diffstat (limited to 'intf')
| -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 |