diff options
author | Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:35 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:35 +0200 |
commit | e4282ea99c664d8d58067bee199cbbcf881b60d5 (patch) | |
tree | d4c4a873eb055c728666f367469fa26c3417793a /parsing/prettyp.ml | |
parent | a0a94c1340a63cdb824507b973393882666ba52a (diff) |
Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg
Diffstat (limited to 'parsing/prettyp.ml')
-rw-r--r-- | parsing/prettyp.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 5543a31c..1e50bc51 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -10,7 +10,7 @@ * on May-June 2006 for implementation of abstraction of pretty-printing of objects. *) -(* $Id: prettyp.ml 11622 2008-11-23 08:45:56Z herbelin $ *) +(* $Id: prettyp.ml 12187 2009-06-13 19:36:59Z msozeau $ *) open Pp open Util @@ -107,8 +107,9 @@ 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 - impl <> [] & let _,lastimpl = list_chop nprods impl in - List.filter is_status_implicit lastimpl <> [] + impl <> [] & List.length impl >= nprods & + let _,lastimpl = list_chop nprods impl in + List.filter is_status_implicit lastimpl <> [] type opacity = | FullyOpaque |