From 75ebf1540b1e53a8ffae43beb5311695bdce8b41 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek
Date: Thu, 4 Mar 2021 20:47:24 +0100
Subject: Add noncritical constraint to exception catching in solve_constraints

---
 proofs/refine.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/refine.ml b/proofs/refine.ml
index ac410a958f..ce04c35e11 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -129,7 +129,6 @@ let solve_constraints =
   tclENV >>= fun env -> tclEVARMAP >>= fun sigma ->
    try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
        Unsafe.tclEVARSADVANCE sigma
-   with e ->
-     (* XXX this is absorbing anomalies? *)
+   with e when CErrors.noncritical e ->
      let info = Exninfo.reify () in
      tclZERO ~info e
-- 
cgit v1.2.3