diff options
author | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-07-23 14:03:56 +0000 |
---|---|---|
committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-07-23 14:03:56 +0000 |
commit | a637b4d1cd7876cb6601a303e69ba7847d42d47e (patch) | |
tree | e8c5944069e733566fc45f800a61aeec599ad033 | |
parent | b978cc7cfd16be8d180a175c0b07d4fa03603212 (diff) |
"Print Setoids" command added.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5968 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | ide/coq_commands.ml | 1 | ||||
-rw-r--r-- | parsing/g_vernacnew.ml4 | 1 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 1 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 1 | ||||
-rw-r--r-- | translate/ppvernacnew.ml | 1 |
5 files changed, 5 insertions, 0 deletions
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index a7309b668..1971fb4f0 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -173,6 +173,7 @@ let state_preserving = [ "Print Module Type"; "Print Modules"; "Print Proof"; + "Print Setoids"; "Print Scope"; "Print Scopes."; "Print Section"; diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 1153a507d..29985d867 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -579,6 +579,7 @@ GEXTEND Gram | IDENT "Hint"; qid = global -> PrintHint qid | IDENT "Hint"; "*" -> PrintHintDb | IDENT "HintDb"; s = IDENT -> PrintHintDbName s + | IDENT "Setoids" -> PrintSetoids | IDENT "Scopes" -> PrintScopes | IDENT "Scope"; s = IDENT -> PrintScope s | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index cfa063e0e..1b87853bd 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -885,6 +885,7 @@ let vernac_print = function | PrintHintGoal -> Auto.print_applicable_hint () | PrintHintDbName s -> Auto.print_hint_db_by_name s | PrintHintDb -> Auto.print_searchtable () + | PrintSetoids -> Setoid_replace.print_setoids() | PrintScopes -> pp (Symbols.pr_scopes (Constrextern.without_symbols pr_rawterm)) | PrintScope s -> diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index a68360235..892b5935e 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -56,6 +56,7 @@ type printable = | PrintHintGoal | PrintHintDbName of string | PrintHintDb + | PrintSetoids | PrintScopes | PrintScope of string | PrintVisibility of string option 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 |