X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=9db77c5d526200246379772cd0a9a1d8cf78c67a;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=a3bc1f39a02a6fb76213c7caf54de0bc798c3a3d;hpb=d7eb6fad3e5afc0fc786c9a91ef64733120dfb43;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index a3bc1f39a..9db77c5d5 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -29,6 +29,7 @@ exception UnificationFailure of string Lazy.t;;
 exception Uncertain of string Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 
+let verbose = false;;
 let debug_print = fun _ -> () 
 
 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
@@ -691,8 +692,9 @@ let fo_unif metasenv context t1 t2 ugraph =
  fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
 
 let enrich_msg msg subst context metasenv t1 t2 ugraph =
- lazy
-  (sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s"
+ lazy (
+  if verbose then
+   sprintf "[Verbose] Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s"
     (CicMetaSubst.ppterm subst t1)
     (try
       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
@@ -711,7 +713,29 @@ let enrich_msg msg subst context metasenv t1 t2 ugraph =
     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
     (CicMetaSubst.ppcontext subst context)
     (CicMetaSubst.ppmetasenv subst metasenv)
-    (CicMetaSubst.ppsubst subst) (Lazy.force msg))
+    (CicMetaSubst.ppsubst subst) (Lazy.force msg)
+ else
+   sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
+    (CicMetaSubst.ppterm_in_context subst t1 context)
+    (try
+      let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
+      CicMetaSubst.ppterm_in_context subst ty_t1 context
+    with 
+    | UnificationFailure s
+    | Uncertain s
+    | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
+    (CicMetaSubst.ppterm_in_context subst t2 context)
+    (try
+      let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
+      CicMetaSubst.ppterm_in_context subst ty_t2 context
+    with
+    | UnificationFailure s
+    | Uncertain s
+    | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
+    (CicMetaSubst.ppcontext subst context)
+    (CicMetaSubst.ppmetasenv subst metasenv)
+    (Lazy.force msg)
+ )
 
 let fo_unif_subst subst context metasenv t1 t2 ugraph =
   try