From 31517149593850a369d4e7d7f1b1fbb34016d4a0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 25 Nov 2014 00:45:20 +0100
Subject: A bit more information in debug tactic unification.

---
 pretyping/unification.ml | 12 ++++++++++--
 1 file 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
 
-- 
cgit v1.2.3