From 8bcf71360261d789ac3ab919bc49309df678628f Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Date: Tue, 2 May 2017 21:32:26 +0200
Subject: labelizing arguments

---
 printing/printer.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 3d67e89f5..1d3e67d9d 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -688,7 +688,7 @@ let default_pr_subgoals ?(pr_first=true)
   let print_multiple_goals g l =
     if pr_first then
       default_pr_goal { it = g ; sigma = sigma; }
-      ++ (if l=[] then str"" else cut ())
+      ++ (if l=[] then mt () else cut ())
       ++ pr_rec 2 l
     else 
       pr_rec 1 (g::l)
-- 
cgit v1.2.3