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

This reverts commit 9b1b5de7a70c54ba3d60560d3d097f3eee2ca907.
---
 printing/pptactic.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 0afe9ae3bf..3ebb370840 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -463,9 +463,10 @@ module Make
 
   let pr_with_induction_names prc = function
     | None, None -> mt ()
-    | Some eqpat, None -> hov 1 (pr_eqn_ipat eqpat)
-    | None, Some ipat -> hov 1 (pr_as_disjunctive_ipat prc ipat)
+    | Some eqpat, None -> spc () ++ hov 1 (pr_eqn_ipat eqpat)
+    | None, Some ipat -> spc () ++ hov 1 (pr_as_disjunctive_ipat prc ipat)
     | Some eqpat, Some ipat ->
+      spc () ++
         hov 1 (pr_as_disjunctive_ipat prc ipat ++ spc () ++ pr_eqn_ipat eqpat)
 
   let pr_as_intro_pattern prc ipat =
-- 
cgit v1.2.3