From 172708b434ead6c3f824cf51e60c3141597e1e2b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 27 Apr 2016 22:13:03 +0200
Subject: Revert "Fixing printing of induction/destruct as."

This reverts commit 691dc7d88c6810333eecef7c2f0b8d8617d19ab1.
---
 printing/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 3ebb370840..06bf077419 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_non_empty_arg (pr_with_induction_names pr.pr_dconstr) ids ++
+                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