aboutsummaryrefslogtreecommitdiffhomepage
path: root/translate
diff options
context:
space:
mode:
authorGravatar sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-07-23 14:03:56 +0000
committerGravatar sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-07-23 14:03:56 +0000
commita637b4d1cd7876cb6601a303e69ba7847d42d47e (patch)
treee8c5944069e733566fc45f800a61aeec599ad033 /translate
parentb978cc7cfd16be8d180a175c0b07d4fa03603212 (diff)
"Print Setoids" command added.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5968 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
-rw-r--r--translate/ppvernacnew.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index b7e739a5c..f4dce4cf0 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -1025,6 +1025,7 @@ let rec pr_vernac = function
| PrintModuleType qid -> str"Print Module Type" ++ spc() ++ pr_reference qid
| PrintModule qid -> str"Print Module" ++ spc() ++ pr_reference qid
| PrintInspect n -> str"Inspect" ++ spc() ++ int n
+ | PrintSetoids -> str"Print Setoids"
| PrintScopes -> str"Print Scopes"
| PrintScope s -> str"Print Scope" ++ spc() ++ str s
| PrintVisibility s -> str"Print Visibility" ++ pr_opt str s