From cc3f28467f826506b8eb6e07c3b2db9ffd2ed3ba Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 27 Apr 2016 22:13:04 +0200
Subject: Revert "Being defensive in printing implicit arguments also with
 manual"

This reverts commit 2211eeda012477b26081738fccc59aa31fb0a565.
---
 interp/constrextern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 2c68a2616..592f59333 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -478,7 +478,7 @@ let explicitize loc inctx impl (cf,f) args =
           (is_needed_for_correct_partial_application tail imp) ||
 	  (!print_implicits_defensive &&
 	   is_significant_implicit a &&
-	   (not (is_inferable_implicit inctx n imp) || !Flags.beautify_file))
+	   not (is_inferable_implicit inctx n imp))
 	in
         if visible then
 	  (a,Some (Loc.ghost, ExplByName (name_of_implicit imp))) :: tail
-- 
cgit v1.2.3