From 1a29faa00f1e2a6f2d71088a769fe2fbc823244a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 2 Mar 2004 06:27:05 +0000
Subject: Correction oubli du cas pas d'arguments implicites du tout

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5414 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/prettyp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index aeca4a9751..85442c0af1 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -86,7 +86,7 @@ let need_expansion impl ref =
   let typ = Global.type_of_global ref in
   let ctx = fst (decompose_prod_assum typ) in
   let nprods = List.length (List.filter (fun (_,b,_) -> b=None) ctx) in
-  let _,lastimpl = list_chop nprods impl in
+  impl <> [] & let _,lastimpl = list_chop nprods impl in
   List.filter is_status_implicit lastimpl <> []
 
 let print_name_infos ref =
-- 
cgit v1.2.3