aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/prettyp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/prettyp.ml')
-rw-r--r--printing/prettyp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 0f6a5e893..0e0480836 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -126,7 +126,7 @@ 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,_) -> Option.is_empty b) ctx) in
- not (List.is_empty impl) && List.length impl >= nprods &
+ not (List.is_empty impl) && List.length impl >= nprods &&
let _,lastimpl = List.chop nprods impl in
List.exists is_status_implicit lastimpl