diff options
| author | sacerdot | 2004-07-23 14:01:44 +0000 |
|---|---|---|
| committer | sacerdot | 2004-07-23 14:01:44 +0000 |
| commit | b978cc7cfd16be8d180a175c0b07d4fa03603212 (patch) | |
| tree | 66d21fb4b8e3d05832975b42a0724e4380132437 | |
| parent | a99671617211f15cce88e0942443d66b07a72db8 (diff) | |
"Show Setoids" command added.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5967 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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) |