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).

---
 proofs/clenv.ml         | 2 +-
 vernac/vernacentries.ml | 7 +++----
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 44d3b44077..b529bba3f5 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -298,7 +298,7 @@ let meta_reducible_instance env evd b =
           if not is_coerce then irec g else u
          with Not_found -> u)
     | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) (* What if two nested casts? *) ->
-      let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) (* idem *) in
+      let m = try destMeta evd c with DestKO -> destMeta evd (pi1 (destCast evd c)) (* idem *) in
           (match
           try
             let g, s = Metamap.find m metas in
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