aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--pretyping/unification.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 3748c7a12..a53240a1c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -996,6 +996,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
if !debug_unification then msg_debug (str "Starting unification");
let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in
+ try
let res =
if occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n
|| subterm_restriction opt flags then None
@@ -1011,7 +1012,6 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
Id.Pred.is_empty dl_id && Cpred.is_empty dl_k)
then error_cannot_unify env sigma (m, n) else None
in
- try
let a = match res with
| Some sigma -> sigma, ms, es
| None -> unirec_rec (env,0) cv_pb opt subst m n in