Remove uses of polymorphic equality from prev. commit

Message to the github robot:
This closes #63

1 files changed, 2 insertions, 2 deletions

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