diff options
author | 2015-05-02 16:56:16 -0400 | |
---|---|---|
committer | 2015-06-22 14:32:19 +0200 | |
commit | 192e683d414ac86d213e2386da40dd7aa5a2fccd (patch) | |
tree | 811cc345be26ce6e8a779986d28b0c1ddc91e899 /toplevel | |
parent | 5089872d20c9e3089676c9267a6394e99cca5121 (diff) |
Guard the List.hd call in [Show Intros]
Fix for [Anomaly: Uncaught exception Failure("hd")] after running [Show
Intros] at the end of a proof:
Goal True. trivial. Show Intros.
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 |