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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

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
-- 
cgit v1.2.3