diff options
| -rw-r--r-- | parsing/prettyp.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index d24f2dd6f6..f00e5f0a1d 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -107,8 +107,9 @@ let need_expansion impl ref = let typ = Global.type_of_global ref in let ctx = (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 |