restore red behaviour printing

3 files changed, 29 insertions, 0 deletions

diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 7bfb2fc210..6704337f80 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -2,30 +2,40 @@ Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
 Arguments Nat.sub _%nat_scope _%nat_scope : simpl nomatch
+The reduction tactics unfold Nat.sub but avoid exposing match constructs
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
 Arguments Nat.sub _%nat_scope / _%nat_scope : simpl nomatch
+The reduction tactics unfold Nat.sub when applied to 1 argument
+  but avoid exposing match constructs
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
 Arguments Nat.sub !_%nat_scope / _%nat_scope : simpl nomatch
+The reduction tactics unfold Nat.sub
+  when the 1st argument evaluates to a constructor and
+  when applied to 1 argument but avoid exposing match constructs
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
 Arguments Nat.sub !_%nat_scope !_%nat_scope /
+The reduction tactics unfold Nat.sub when the 1st and
+  2nd arguments evaluate to a constructor and when applied to 2 arguments
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
 Arguments Nat.sub !_%nat_scope !_%nat_scope
+The reduction tactics unfold Nat.sub when the 1st and
+  2nd arguments evaluate to a constructor
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 pf :
@@ -34,18 +44,21 @@ forall D1 C1 : Type,
 
 pf is not universe polymorphic
 Arguments pf {D1%foo_scope} {C1%type_scope} _ [D2] [C2] : simpl never
+The reduction tactics never unfold pf
 pf is transparent
 Expands to: Constant Arguments.pf
 fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
 
 fcomp is not universe polymorphic
 Arguments fcomp {A%type_scope} {B%type_scope} {C%type_scope} _ _ _ /
+The reduction tactics unfold fcomp when applied to 6 arguments
 fcomp is transparent
 Expands to: Constant Arguments.fcomp
 volatile : nat -> nat
 
 volatile is not universe polymorphic
 Arguments volatile / _%nat_scope
+The reduction tactics always unfold volatile
 volatile is transparent
 Expands to: Constant Arguments.volatile
 f : T1 -> T2 -> nat -> unit -> nat -> nat
@@ -58,18 +71,24 @@ f : T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
 Arguments f _ _ !_%nat_scope !_ !_%nat_scope
+The reduction tactics unfold f when the 3rd, 4th and
+  5th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.S1.S2.f
 f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
 Arguments f [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope
+The reduction tactics unfold f when the 4th, 5th and
+  6th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.S1.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
 Arguments f [T1%type_scope] [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope
+The reduction tactics unfold f when the 5th, 6th and
+  7th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.f
      = forall v : unit, f 0 0 5 v 3 = 2
@@ -80,6 +99,8 @@ f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
 Arguments f _ _ _ _ !_ !_ !_
+The reduction tactics unfold f when the 5th, 6th and
+  7th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.f
 forall w : r, w 3 true = tt
@@ -94,6 +115,8 @@ volatilematch : nat -> nat
 
 volatilematch is not universe polymorphic
 Arguments volatilematch / _%nat_scope : simpl nomatch
+The reduction tactics always unfold volatilematch
+  but avoid exposing match constructs
 volatilematch is transparent
 Expands to: Constant Arguments.volatilematch
      = fun n : nat => volatilematch n
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index e025c167e3..53d5624f6f 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -42,6 +42,8 @@ myplus : forall T : Type, T -> nat -> nat -> nat
 
 myplus is not universe polymorphic
 Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
+The reduction tactics unfold myplus when the 2nd and
+  3rd arguments evaluate to a constructor
 myplus is transparent
 Expands to: Constant Arguments_renaming.Test1.myplus
 @myplus
@@ -71,6 +73,8 @@ myplus : forall T : Type, T -> nat -> nat -> nat
 
 myplus is not universe polymorphic
 Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
+The reduction tactics unfold myplus when the 2nd and
+  3rd arguments evaluate to a constructor
 myplus is transparent
 Expands to: Constant Arguments_renaming.myplus
 @myplus
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)])