Merge PR #7099: Stronger invariants in unification signature.

1 files changed, 4 insertions, 3 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 218b2671ec..95c30d8159 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -309,9 +309,10 @@ let check_meta_variables env sigma c =
 
 let check_conv_leq_goal env sigma arg ty conclty =
   if !check then
-    let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
-      if b then evm 
-      else raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
+    let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
+    match ans with
+    | Some evm -> evm
+    | None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
   else sigma
 
 exception Stop of EConstr.t list