diff options
| author | letouzey | 2001-09-17 14:35:57 +0000 |
|---|---|---|
| committer | letouzey | 2001-09-17 14:35:57 +0000 |
| commit | 2a880279eaf97f0b2bc5dd76220c5516df78b774 (patch) | |
| tree | 9aed0ab6737e80741b3acdc9041710ad69a070a1 | |
| parent | d52de91b333e0c4bc0c326288757e89c341eb28c (diff) | |
Blindage de Show Intro
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1976 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/vernacentries.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 7618aadd71..71740fbd9e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1791,8 +1791,11 @@ let _ = vinterp_add "SHOWINTRO" let pf = get_pftreestate() in let gl = nth_goal_of_pftreestate 1 pf in let l,_= decompose_prod (strip_outer_cast (pf_concl gl)) in - let n = List.hd (List.rev_map fst l) in - message (string_of_id (fresh_id [] (id_of_name n) gl))) + try + let n = + List.hd (List.rev_map fst l) in + message (string_of_id (fresh_id [] (id_of_name n) gl)) + with Failure "hd" -> message "") | _ -> bad_vernac_args "Show Intro") let _ = vinterp_add "SHOWINTROS" |