diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 17 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 17 | ||||
| -rw-r--r-- | parsing/prettyp.ml | 6 |
3 files changed, 33 insertions, 7 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 2efe88c0c..27f80fd75 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -446,9 +446,13 @@ GEXTEND Gram gallina_ext: [ [ (* Transparent and Opaque *) - IDENT "Transparent"; l = LIST1 global -> VernacSetOpacity (false, l) - | IDENT "Opaque"; l = LIST1 global -> VernacSetOpacity (true, l) - + IDENT "Transparent"; l = LIST1 global -> + VernacSetOpacity [Conv_oracle.transparent,l] + | IDENT "Opaque"; l = LIST1 global -> + VernacSetOpacity [Conv_oracle.Opaque, l] + | IDENT "Strategy"; l = + LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] -> + VernacSetOpacity l (* Canonical structure *) | IDENT "Canonical"; IDENT "Structure"; qid = global -> VernacCanonical qid @@ -542,6 +546,13 @@ GEXTEND Gram [ [ ":="; l = LIST1 typeclass_field_def SEP ";" -> l | -> [] ] ] ; + strategy_level: + [ [ IDENT "expand" -> Conv_oracle.Expand + | IDENT "opaque" -> Conv_oracle.Opaque + | n=INT -> Conv_oracle.Level (int_of_string n) + | "-"; n=INT -> Conv_oracle.Level (- int_of_string n) + | IDENT "transparent" -> Conv_oracle.transparent ] ] + ; END GEXTEND Gram diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index a863665a9..afa28768f 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -829,9 +829,22 @@ 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 (fl,l) -> - hov 1 ((if fl then str"Opaque" else str"Transparent") ++ + | VernacSetOpacity[k,l] when k=Conv_oracle.transparent -> + hov 1 (str"Transparent" ++ spc() ++ prlist_with_sep sep pr_reference l) + | VernacSetOpacity[Conv_oracle.Opaque,l] -> + hov 1 (str"Opaque" ++ + spc() ++ prlist_with_sep sep pr_reference l) + | VernacSetOpacity l -> + let pr_lev = function + Conv_oracle.Opaque -> str"opaque" + | Conv_oracle.Expand -> str"expand" + | l when l = Conv_oracle.transparent -> str"transparent" + | Conv_oracle.Level n -> int n in + 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)) | VernacUnsetOption na -> hov 1 (str"Unset" ++ spc() ++ pr_printoption na None) | VernacSetOption (na,v) -> hov 2 (str"Set" ++ spc() ++ pr_set_option na v) diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 6ca3a5c1a..dc242e8ca 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -116,12 +116,14 @@ type opacity = let opacity env = function | VarRef v when pi2 (Environ.lookup_named v env) <> None -> - Some (TransparentMaybeOpacified (Conv_oracle.is_opaque_var v)) + Some (TransparentMaybeOpacified + (not (Reductionops.is_transparent(VarKey v)))) | ConstRef cst -> let cb = Environ.lookup_constant cst env in if cb.const_body = None then None else if cb.const_opaque then Some FullyOpaque - else Some (TransparentMaybeOpacified (Conv_oracle.is_opaque_cst cst)) + else Some (TransparentMaybeOpacified + (not(Reductionops.is_transparent(ConstKey cst)))) | _ -> None let print_opacity ref = |