diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 188d2d098f31..c4be56f53a2e 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