diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-22 17:12:11 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-22 17:12:11 +0000 |
| commit | 9bf1f84def4e7635dd5b81038e5d76ee2a77204e (patch) | |
| tree | 4ac2cf352a6daf61f8efe70c658e3980a52c93af /parsing/ppvernac.ml | |
| parent | 96876c750e05108e07dc1f29fa8db53f35f62f95 (diff) | |
Strategy commands are now exported
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10971 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/ppvernac.ml')
| -rw-r--r-- | parsing/ppvernac.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index afa28768f..c31defe09 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -829,13 +829,13 @@ let rec pr_vernac = function str (if List.length idl > 1 then "s " else " ") ++ prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++ pr_lconstr c) - | VernacSetOpacity[k,l] when k=Conv_oracle.transparent -> + | VernacSetOpacity(true,[k,l]) when k=Conv_oracle.transparent -> hov 1 (str"Transparent" ++ spc() ++ prlist_with_sep sep pr_reference l) - | VernacSetOpacity[Conv_oracle.Opaque,l] -> + | VernacSetOpacity(true,[Conv_oracle.Opaque,l]) -> hov 1 (str"Opaque" ++ spc() ++ prlist_with_sep sep pr_reference l) - | VernacSetOpacity l -> + | VernacSetOpacity (local,l) -> let pr_lev = function Conv_oracle.Opaque -> str"opaque" | Conv_oracle.Expand -> str"expand" @@ -844,7 +844,8 @@ let rec pr_vernac = function let pr_line (l,q) = hov 2 (pr_lev l ++ spc() ++ str"[" ++ prlist_with_sep sep pr_reference q ++ str"]") in - hov 1 (str"Strategy" ++ spc() ++ hv 0 (prlist_with_sep sep pr_line l)) + hov 1 (pr_locality local ++ str"Strategy" ++ spc() ++ + hv 0 (prlist_with_sep sep pr_line l)) | VernacUnsetOption na -> hov 1 (str"Unset" ++ spc() ++ pr_printoption na None) | VernacSetOption (na,v) -> hov 2 (str"Set" ++ spc() ++ pr_set_option na v) |