From 2211eeda012477b26081738fccc59aa31fb0a565 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 10 Apr 2016 18:31:25 +0200
Subject: Being defensive in printing implicit arguments also with manual
 implicit arguments when in beautification mode.

---
 interp/constrextern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 592f59333..2c68a2616 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))
+	   (not (is_inferable_implicit inctx n imp) || !Flags.beautify_file))
 	in
         if visible then
 	  (a,Some (Loc.ghost, ExplByName (name_of_implicit imp))) :: tail
-- 
cgit v1.2.3