From 9374aeeda2a3bc64774753862eae39a8e8539bb7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 4 Nov 2020 07:30:40 +0100
Subject: One catch-all's missing a noncritical; another is now useless (see
 7efaf86).

---
 vernac/vernacentries.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e8d84a67a3..af40292f18 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1934,10 +1934,9 @@ let vernac_search ~pstate ~atts s gopt r =
   let open ComSearch in
   let gopt = query_command_selector gopt in
   let sigma, env =
-    match gopt with | None ->
-      (* 1st goal by default if it exists, otherwise no goal at all *)
-      (try get_goal_or_global_context ~pstate 1
-       with _ -> let env = Global.env () in (Evd.from_env env, env))
+    match gopt with
+    (* 1st goal by default if it exists, otherwise no goal at all *)
+    | None -> get_goal_or_global_context ~pstate 1
     (* if goal selector is given and wrong, then let exceptions be raised. *)
     | Some g -> get_goal_or_global_context ~pstate g in
   interp_search env sigma s r
-- 
cgit v1.2.3