diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-06-03 10:59:01 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-06-03 10:59:01 +0000 |
| commit | 3ebb022b83193383475a0ef3c1e79fc93cf3e800 (patch) | |
| tree | a68d667b08a53bf7437cb38b32e15bb565eb7a5a | |
| parent | c061913fe807331d46baf9f807d7010806a82240 (diff) | |
Affichage de l'opacité par About mais pas par Print (compatibilité coq'art)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5802 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/prettyp.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index e3735c718..9ca46afb7 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -109,8 +109,8 @@ let print_opacity ref = | Some s -> pr_global ref ++ str " is " ++ str (match s with | FullyOpaque -> "opaque" - | TransparentMaybeOpacified true -> "basically transparent (but considered opaque for reduction)" - | TransparentMaybeOpacified false -> "transparent") + | TransparentMaybeOpacified true -> "basically transparent but considered opaque for reduction" + | TransparentMaybeOpacified false -> "transparent") ++ fnl() let print_name_infos ref = let impl = implicits_of_global ref in @@ -127,7 +127,6 @@ let print_name_infos ref = else mt()) ++ type_for_implicit ++ print_impl_args impl ++ print_argument_scopes scopes - ++ print_opacity ref let print_id_args_data test pr id l = if List.exists test l then @@ -519,9 +518,12 @@ let print_about ref = let sigma = Evd.empty in let k = locate_any_name ref in begin match k with - | Term ref -> print_ref false ref ++ print_name_infos ref - | Syntactic kn -> print_syntactic_def " := " kn - | Dir _ | ModuleType _ | Undefined _ -> mt () end + | Term ref -> + print_ref false ref ++ print_name_infos ref ++ print_opacity ref + | Syntactic kn -> + print_syntactic_def " := " kn + | Dir _ | ModuleType _ | Undefined _ -> + mt () end ++ hov 0 (str "Expands to: " ++ pr_located_qualid k) |