diff options
| author | Hugo Herbelin | 2014-11-25 00:45:20 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-25 11:25:22 +0100 |
| commit | 31517149593850a369d4e7d7f1b1fbb34016d4a0 (patch) | |
| tree | 4213194ab85543eae61662a9c7f8151df9a6f829 | |
| parent | 3a8cc0551c35489a34ef64d416b7200a29403a33 (diff) | |
A bit more information in debug tactic unification.
| -rw-r--r-- | pretyping/unification.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index df9046f152..8009bad2de 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -975,6 +975,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb else error_cannot_unify (fst curenvnb) sigma (cM,cN) in + if !debug_unification then msg_debug (str "Starting unification"); let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in let res = if occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n @@ -991,9 +992,16 @@ 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 - match res with + try + let a = match res with | Some sigma -> sigma, ms, es - | None -> unirec_rec (env,0) cv_pb opt subst m n + | None -> unirec_rec (env,0) cv_pb opt subst m n in + if !debug_unification then msg_debug (str "Leaving unification with success"); + a + with e -> + if !debug_unification then msg_debug (str "Leaving unification with failure"); + raise e + let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env |