diff options
Diffstat (limited to 'plugins/interface/ascent.mli')
| -rw-r--r-- | plugins/interface/ascent.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/interface/ascent.mli b/plugins/interface/ascent.mli index f0b68fb7c1..bc615f14ec 100644 --- a/plugins/interface/ascent.mli +++ b/plugins/interface/ascent.mli @@ -107,6 +107,7 @@ and ct_COMMAND = | CT_mind_decl of ct_CO_IND * ct_IND_SPEC_LIST | CT_ml_add_path of ct_STRING | CT_ml_declare_modules of ct_STRING_NE_LIST + | CT_local_ml_declare_modules of ct_STRING_NE_LIST | CT_ml_print_modules | CT_ml_print_path | CT_module of ct_ID * ct_MODULE_BINDER_LIST * ct_MODULE_TYPE_CHECK * ct_MODULE_EXPR |