X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=344e7535c2614e2d971cd798326f9fba918a760d;hb=d1c9cdb2de96aa2dda6a7b25a4c4959b82b08f6c;hp=c1b5c302f2b5a27147eff1c629c4558fca12f516;hpb=a3417bd94b857a7f96a2221ba5b79444823b2144;p=helm.git

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index c1b5c302f..344e7535c 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -578,6 +578,8 @@ let smart_apply t unit_eq status g =
         debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
         fast_eq_check unit_eq status j
     with
+      | NCicEnvironment.ObjectNotFound s as e ->
+          raise (Error (lazy "eq_coerc non yet defined",Some e))
       | Error _ as e -> debug_print (lazy "error"); raise e
 
 let smart_apply_tac t s =