diff options
| author | Gaëtan Gilbert | 2019-10-30 16:30:26 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-31 14:42:54 +0100 |
| commit | 777109f0068d524ca2a82d405416da273fec3d7f (patch) | |
| tree | 8fe1a56d8049b4a1af508c0a6c6f9991d8394798 /vernac | |
| parent | d9892ecc6cc647ffc8803b17350f46ce6b901410 (diff) | |
restore red behaviour printing
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/prettyp.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 358c40bdb0..b03ff7b2ae 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -884,11 +884,13 @@ let print_about_any ?loc env sigma k udecl = maybe_error_reject_univ_decl k udecl; match k with | Term ref -> + let rb = Reductionops.ReductionBehaviour.print ref in Dumpglob.add_glob ?loc ref; pr_infos_list (print_ref false ref udecl :: blankline :: print_polymorphism ref @ print_name_infos ref @ + (if Pp.ismt rb then [] else [rb]) @ print_opacity ref @ print_bidi_hints ref @ [hov 0 (str "Expands to: " ++ pr_located_qualid k)]) |