diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-08 07:58:01 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-08 07:58:01 +0000 |
| commit | 8de569861cb8c3ebc697026c43c583a54bae6ce5 (patch) | |
| tree | 282ba082d2eafe3ea5fa4c80e67be6f03f94000f /translate | |
| parent | a330ee4a6e399824294887cbb1f496c7ed5a8208 (diff) | |
Ajout option "Local" à "Open Scope"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3867 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppvernacnew.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 8e7aa2fc1..76771ece7 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -415,7 +415,8 @@ let rec pr_vernac = function | VernacTacticGrammar l -> hov 1 (str"Grammar tactic simple_tactic :=" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"|") pr_grammar_tactic_rule l) (***) | VernacSyntax (u,el) -> hov 1 (str"Syntax " ++ str u ++ spc() ++ prlist_with_sep sep_v2 pr_syntax_entry el) (***) - | VernacOpenScope sc -> str"Open Scope" ++ spc() ++ str sc + | VernacOpenScope (exp,sc) -> + str ("Open "^(if exp then "" else "Local ")^"Scope") ++ spc() ++ str sc | VernacDelimiters (sc,key) -> str"Delimits Scope" ++ spc () ++ str sc ++ spc() ++ str "with " ++ str key |