removing extra spaces

[helm.git] / matita / components / ng_tactics / nnAuto.ml

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 25274de814f7571774f7ee3a5df6054e0ca668b5..b77c633694404c00e155d6d102cbaca41645355d 100644 (file)
--- 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 =
@@ -1883,23 +1887,3 @@ let auto_tac ~params:(_,flags as params) ?trace_ref =
     fast_eq_check_tac ~params  
   else auto_tac ~params ?trace_ref
 ;;
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-