From 896dbb726688866298fd7bbea98e3d7d0391bc75 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 28 Jul 2010 16:43:39 +0000
Subject: [PATCH] allows auto before eq is defined

---
 helm/software/components/ng_tactics/nnAuto.ml | 2 ++
 1 file changed, 2 insertions(+)

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 =
-- 
2.39.2