Fix output test-suite 'simpl tactic' -> 'reduction tactics'

4 files changed, 19 insertions, 18 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index bbd5c35207..f9fe53fdf6 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -430,13 +430,13 @@ let prlist_sep_lastsep no_empty sep lastsep elem =
     |[] -> mt ()
     |[e] -> elem e
     |h::t -> let e = elem h in
-	if no_empty && e = mt () then start t else
+	if no_empty && ismt e then start t else
 	  let rec aux = function
 	    |[] -> mt ()
 	    |h::t ->
 	       let e = elem h and r = aux t in
-		 if no_empty && e = mt () then r else
-		   if r = mt ()
+		 if no_empty && ismt e then r else
+		   if ismt r
 		   then let s = lastsep () in s ++ e
 		   else let s = sep () in s ++ e ++ r
 	  in let r = aux t in e ++ r
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 031db5b0c8..89808ef4db 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -635,11 +635,12 @@ let print_opaque_name qid =
 let print_about_any loc k =
   match k with
   | Term ref ->
+    let rb = Reductionops.ReductionBehaviour.print ref in
     Dumpglob.add_glob loc ref;
       pr_infos_list
        (print_ref false ref :: blankline ::
 	print_name_infos ref @
-	Reductionops.ReductionBehaviour.print ref ::
+	(if Pp.ismt rb then [] else [rb]) @
 	print_opacity ref @
 	[hov 0 (str "Expands to: " ++ pr_located_qualid k)])
   | Syntactic kn ->
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index f5636fbf9d..d1a6be9bdb 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -1,20 +1,20 @@
 minus : nat -> nat -> nat
 
 Argument scopes are [nat_scope nat_scope]
-The simpl tactic unfolds minus avoiding to expose match constructs
+The reduction tactics unfold minus avoiding to expose match constructs
 minus is transparent
 Expands to: Constant Coq.Init.Peano.minus
 minus : nat -> nat -> nat
 
 Argument scopes are [nat_scope nat_scope]
-The simpl tactic unfolds minus when applied to 1 argument
+The reduction tactics unfold minus when applied to 1 argument
   avoiding to expose match constructs
 minus is transparent
 Expands to: Constant Coq.Init.Peano.minus
 minus : nat -> nat -> nat
 
 Argument scopes are [nat_scope nat_scope]
-The simpl tactic unfolds minus
+The reduction tactics unfold minus
   when the 1st argument evaluates to a constructor and
   when applied to 1 argument avoiding to expose match constructs
 minus is transparent
@@ -22,14 +22,14 @@ Expands to: Constant Coq.Init.Peano.minus
 minus : nat -> nat -> nat
 
 Argument scopes are [nat_scope nat_scope]
-The simpl tactic unfolds minus when the 1st and
+The reduction tactics unfold minus when the 1st and
   2nd arguments evaluate to a constructor and when applied to 2 arguments 
 minus is transparent
 Expands to: Constant Coq.Init.Peano.minus
 minus : nat -> nat -> nat
 
 Argument scopes are [nat_scope nat_scope]
-The simpl tactic unfolds minus when the 1st and
+The reduction tactics unfold minus when the 1st and
   2nd arguments evaluate to a constructor 
 minus is transparent
 Expands to: Constant Coq.Init.Peano.minus
@@ -40,20 +40,20 @@ forall D1 C1 : Type,
 Arguments D2, C2 are implicit
 Arguments D1, C1 are implicit and maximally inserted
 Argument scopes are [foo_scope type_scope _ _ _ _ _]
-The simpl tactic never unfolds pf
+The reduction tactics never unfold pf
 pf is transparent
 Expands to: Constant Top.pf
 fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
 
 Arguments A, B, C are implicit and maximally inserted
 Argument scopes are [type_scope type_scope type_scope _ _ _]
-The simpl tactic unfolds fcomp when applied to 6 arguments 
+The reduction tactics unfold fcomp when applied to 6 arguments 
 fcomp is transparent
 Expands to: Constant Top.fcomp
 volatile : nat -> nat
 
 Argument scope is [nat_scope]
-The simpl tactic always unfolds volatile
+The reduction tactics always unfold volatile
 volatile is transparent
 Expands to: Constant Top.volatile
 f : T1 -> T2 -> nat -> unit -> nat -> nat
@@ -64,7 +64,7 @@ Expands to: Constant Top.S1.S2.f
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
 Argument scopes are [_ _ nat_scope _ nat_scope]
-The simpl tactic unfolds f when the 3rd, 4th and
+The reduction tactics unfold f when the 3rd, 4th and
   5th arguments evaluate to a constructor 
 f is transparent
 Expands to: Constant Top.S1.S2.f
@@ -72,7 +72,7 @@ f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 Argument T2 is implicit
 Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
-The simpl tactic unfolds f when the 4th, 5th and
+The reduction tactics unfold f when the 4th, 5th and
   6th arguments evaluate to a constructor 
 f is transparent
 Expands to: Constant Top.S1.f
@@ -80,13 +80,13 @@ f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 Arguments T1, T2 are implicit
 Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
-The simpl tactic unfolds f when the 5th, 6th and
+The reduction tactics unfold f when the 5th, 6th and
   7th arguments evaluate to a constructor 
 f is transparent
 Expands to: Constant Top.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
-The simpl tactic unfolds f when the 5th, 6th and
+The reduction tactics unfold f when the 5th, 6th and
   7th arguments evaluate to a constructor 
 f is transparent
 Expands to: Constant Top.f
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 5273c59ecb..695efb260d 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -55,7 +55,7 @@ myplus : forall T : Type, T -> nat -> nat -> nat
 Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
-The simpl tactic unfolds myplus when the 2nd and
+The reduction tactics unfold myplus when the 2nd and
   3rd arguments evaluate to a constructor 
 myplus is transparent
 Expands to: Constant Top.Test1.myplus
@@ -92,7 +92,7 @@ myplus : forall T : Type, T -> nat -> nat -> nat
 Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
-The simpl tactic unfolds myplus when the 2nd and
+The reduction tactics unfold myplus when the 2nd and
   3rd arguments evaluate to a constructor 
 myplus is transparent
 Expands to: Constant Top.myplus