From 2e1b90f8b0a585c4a4dd65ffd4b297442cc66cc8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 16 Sep 2014 09:41:17 +0200
Subject: More on printing references applied to implicit arguments.

---
 interp/constrextern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f71cf5a65b..2e6ab43544 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -460,7 +460,7 @@ let is_projection primprojapp nargs cf =
       | _ -> None, None
       
 	
-let is_hole = function CHole _ -> true | _ -> false
+let is_hole = function CHole _ | CEvar _ -> true | _ -> false
 
 let is_significant_implicit a =
   not (is_hole a)
@@ -547,7 +547,7 @@ let explicitize loc inctx impl (cf,primprojapp,f) args =
 	CAppExpl (loc, (ip, f', us), args)
 
 let is_start_implicit = function
-  | imp :: _ -> is_status_implicit imp (* && maximal_insertion_of imp *)
+  | imp :: _ -> is_status_implicit imp && maximal_insertion_of imp
   | [] -> false
 
 let extern_global loc impl f us =
-- 
cgit v1.2.3