From af4283e8e4e670b8a5761892548f2d65792cd7e9 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Tue, 16 Aug 2011 09:29:36 +0000
Subject: Fixes bug #2587 (Print Hint gives anomaly when no focused subgoals)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14411 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/auto.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/tactics/auto.ml b/tactics/auto.ml
index fb61fffd1d..1f3f5a076c 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -806,8 +806,11 @@ let print_hint_term cl = ppnl (pr_hint_term cl)
 let print_applicable_hint () =
   let pts = get_pftreestate () in
   let glss = Proof.V82.subgoals pts in
-  let gl = { Evd.it = List.hd glss.Evd.it; sigma = glss.Evd.sigma } in
-  print_hint_term (pf_concl gl)
+  match glss.Evd.it with
+  | [] -> Util.error "No focused goal."
+  | g::_ ->
+    let gl = { Evd.it = g; sigma = glss.Evd.sigma } in
+    print_hint_term (pf_concl gl)
 
 (* displays the whole hint database db *)
 let print_hint_db db =
-- 
cgit v1.2.3