diff options
| -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 |