From d78784bd86d3d571bb2891356e9e9718c69976ba Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 10 Apr 2016 14:30:25 +0200
Subject: Fixing printing of "destruct in" after ce71ac17268f.

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

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 3cff541b06..19536d9f83 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -878,7 +878,7 @@ module Make
             ++ prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) ->
               pr_clear_flag clear_flag (pr_induction_arg pr.pr_dconstr pr.pr_dconstr) h ++
                 pr_with_induction_names pr.pr_dconstr ids ++
-                pr_opt_no_spc (pr_clauses None pr.pr_name) cl) l ++
+                pr_opt (pr_clauses None pr.pr_name) cl) l ++
               pr_opt pr_eliminator el
           )
         | TacDoubleInduction (h1,h2) ->
-- 
cgit v1.2.3