diff options
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 86ba38186c..80fe26a817 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -102,13 +102,13 @@ let try_print_subgoals () = let show_intro all = let pf = get_pftreestate() in let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in - if gls <> [] then begin + if not (List.is_empty gls) then begin let gl = {Evd.it=List.hd gls ; sigma = sigma; } in let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in if all then let lid = Tactics.find_intro_names l gl in msg_notice (hov 0 (prlist_with_sep spc pr_id lid)) - else if l <> [] then + else if not (List.is_empty l) then let n = List.last l in msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl))) end |