diff options
| -rw-r--r-- | pretyping/unification.ml | 2 |
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 |