X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=c42ab8b2759d8493bd7396c1f2262c26e2593fd6;hb=9afdb35b870c15760f482a1b4a0ad7b4dcd5172b;hp=25274de814f7571774f7ee3a5df6054e0ca668b5;hpb=6f1f9e20aa2775d41bba64289fc903e6612baaf3;p=helm.git

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 25274de81..c42ab8b27 100644
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -632,6 +632,10 @@ let smart_apply t unit_eq status g =
       | NCicEnvironment.ObjectNotFound s as e ->
           raise (Error (lazy "eq_coerc non yet defined",Some e))
       | Error _ as e -> debug_print (lazy "error"); raise e
+(* FG: for now we catch TypeCheckerFailure; to be understood *)  
+      | NCicTypeChecker.TypeCheckerFailure _ ->
+          debug_print (lazy "TypeCheckerFailure");
+          raise (Error (lazy "no proof found",None))
 ;;
 
 let compare_statuses ~past ~present =