From 192e683d414ac86d213e2386da40dd7aa5a2fccd Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel
Date: Sat, 2 May 2015 16:56:16 -0400
Subject: Guard the List.hd call in [Show Intros]

Fix for [Anomaly: Uncaught exception Failure("hd")] after running [Show
Intros] at the end of a proof:

    Goal True. trivial. Show Intros.
---
 toplevel/vernacentries.ml | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 188d2d098f..c4be56f53a 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
-- 
cgit v1.2.3


From d6ee11ac2190df5adad63e5125a9e583533e49e0 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel
Date: Sat, 2 May 2015 17:36:05 -0400
Subject: Replace 'try ... with Failure "List.last"' with 'if l <> []'

---
 toplevel/vernacentries.ml | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c4be56f53a..86ba38186c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -105,16 +105,13 @@ let show_intro all =
   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
+    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
+    else if l <> [] then
+      let n = List.last l in
+      msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl)))
+  end
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
-- 
cgit v1.2.3


From 4b6b4d8cdd12902d166504ec3d96ca94705d81f6 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel
Date: Mon, 4 May 2015 14:26:24 -0400
Subject: Remove uses of polymorphic equality from prev. commit

Message to the github robot:
This closes #63
---
 toplevel/vernacentries.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 86ba38186c..80fe26a817 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -102,13 +102,13 @@ let try_print_subgoals () =
 let show_intro all =
   let pf = get_pftreestate() in
   let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
-  if gls <> [] then begin
+  if not (List.is_empty 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 if l <> [] then
+    else if not (List.is_empty l) then
       let n = List.last l in
       msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl)))
   end
-- 
cgit v1.2.3