From 7d9eb40cad437c9a6bfe7eea588ca56cc50ed3ed Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 16 Apr 2003 16:51:40 +0000
Subject: On force l'affichage des implicites non '?' lors de la traduction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3926 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrextern.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e3edd8cbac..d07934f7dd 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -162,7 +162,9 @@ let explicitize loc inctx impl f args =
         let tail = exprec (q+1) (args,impl) in
         let visible =
           (!print_implicits & !print_implicits_explicit_args)
-          or not (is_inferable_implicit inctx n imp) in
+          or not (is_inferable_implicit inctx n imp)
+          or ((match a with CHole _ -> false | _ -> true)
+              & Options.do_translate()) in
         if visible then (a,Some q) :: tail else tail
     | a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl)
     | args, [] -> List.map (fun a -> (a,None)) args (*In case of polymorphism*)
-- 
cgit v1.2.3