diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 188d2d098..c4be56f53 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -102,17 +102,19 @@ let try_print_subgoals () = let show_intro all = let pf = get_pftreestate() in let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in - 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 - try - let n = List.last l in - msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl))) - with Failure "List.last" -> () + if 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 + try + let n = List.last l in + msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl))) + with Failure "List.last" -> () + end (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name |