diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-16 09:29:36 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-16 09:29:36 +0000 |
| commit | af4283e8e4e670b8a5761892548f2d65792cd7e9 (patch) | |
| tree | 14fad8d078fa9a2d191bda297e075dcf66acc34d | |
| parent | e031aaf7d7412884315c08e64816fa43ce8794ca (diff) | |
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
| -rw-r--r-- | tactics/auto.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index fb61fffd1..1f3f5a076 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 = |