From d99fe37fc4b348fd86ac836cbe4166ef28ed34c2 Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Tue, 25 Feb 2014 18:44:00 +0100
Subject: Fix output test-suite 'simpl tactic' -> 'reduction tactics'

---
 printing/prettyp.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'printing')

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 ->
-- 
cgit v1.2.3