Added "nocomposites" to coercions.

[helm.git] / matita / components / ng_refiner / nCicUnification.ml

diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml
index 1e37ff79793ba03894f306c0be69acb50bbe7115..c8f67f1769e523fd53df6f7c067d99c68bcfa915 100644 (file)
--- a/matita/components/ng_refiner/nCicUnification.ml
+++ b/matita/components/ng_refiner/nCicUnification.ml
@@ -99,6 +99,8 @@ let outside exc_opt =
     match !times with time1::tl -> times := tl; time1 | [] -> assert false in
    prerr_endline ("}}} " ^ !indent ^ " " ^ string_of_float (time2 -. time1));
    (match exc_opt with
+   | Some (UnificationFailure msg) ->  prerr_endline ("exception raised: NCicUnification.UnificationFailure:" ^ Lazy.force msg)
+   | Some (Uncertain msg) ->  prerr_endline ("exception raised: NCicUnification.Uncertain:" ^ Lazy.force msg)
    | Some e ->  prerr_endline ("exception raised: " ^ Printexc.to_string e)
    | None -> ());
    try