From 11919074c08a64e78e5a5581d744332a093850f0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 5 Dec 2014 11:22:51 +0100 Subject: Fix debugger Tactic Unification. --- pretyping/unification.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- cgit v1.2.3