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'

---
 lib/pp.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'lib')

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