From 691dc7d88c6810333eecef7c2f0b8d8617d19ab1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Apr 2016 16:12:04 +0200
Subject: Fixing printing of induction/destruct as.

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

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 06bf077419..3ebb370840 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -863,7 +863,7 @@ module Make
             ++ spc ()
             ++ 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_non_empty_arg (pr_with_induction_names pr.pr_dconstr) ids ++
                 pr_opt (pr_clauses None pr.pr_name) cl) l ++
               pr_opt pr_eliminator el
           )
-- 
cgit v1.2.3