From 9b1b5de7a70c54ba3d60560d3d097f3eee2ca907 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 16 Apr 2016 22:09:24 +0200
Subject: Fixing extra space in printing destruct/induction as.

---
 printing/pptactic.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

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