From 2a880279eaf97f0b2bc5dd76220c5516df78b774 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 17 Sep 2001 14:35:57 +0000
Subject: Blindage de Show Intro

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1976 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 7 +++++--
 1 file 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"
-- 
cgit v1.2.3