diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/ascent.mli | 1 | ||||
| -rw-r--r-- | contrib/interface/vtp.ml | 1 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 1 |
3 files changed, 3 insertions, 0 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index 61d0d5a3af..d246e73236 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -135,6 +135,7 @@ and ct_COMMAND = | CT_print_opaqueid of ct_ID | CT_print_path of ct_ID * ct_ID | CT_print_proof of ct_ID + | CT_print_setoids | CT_print_scope of ct_ID | CT_print_scopes | CT_print_section of ct_ID diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index ff41852380..675b024ce6 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -451,6 +451,7 @@ and fCOMMAND = function | CT_print_scope(x1) -> fID x1; fNODE "print_scope" 1 +| CT_print_setoids -> fNODE "print_setoids" 0 | CT_print_scopes -> fNODE "print_scopes" 0 | CT_print_section(x1) -> fID x1; diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index d2562e9781..a333957aaf 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1777,6 +1777,7 @@ let rec xlate_vernac = | PrintInspect n -> CT_inspect (CT_int n) | PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s) | PrintLocalContext -> CT_print + | PrintSetoids -> CT_print_setoids | PrintTables -> CT_print_tables | PrintModuleType a -> CT_print_module_type (loc_qualid_to_ct_ID a) | PrintModule a -> CT_print_module (loc_qualid_to_ct_ID a) |