X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=a384d54d56259f89952a7a14f8d013022cee568a;hb=d268de514258947484a22a106c220b102c611cc3;hp=fc0a8013cca3b09deb1b8ab9703499dc0f66d4f5;hpb=f4c17198d8afe7c8cd62dbab527d08902d891491;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index fc0a8013c..a384d54d5 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -601,11 +601,13 @@ let auto ~params:(l,_) status goal =
         (status, (t,ty) :: l))
       (status,[]) l
   in
-  let pt, metasenv, subst = 
-    Paramod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
-  in      
-  let status = status#set_obj (n,h,metasenv,subst,o) in
-  instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
+  match
+    NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
+  with
+  | [] -> raise (NTacStatus.Error (lazy "no proof found",None))
+  | (pt, metasenv, subst)::_ -> 
+      let status = status#set_obj (n,h,metasenv,subst,o) in
+      instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
 ;;
 
 let auto_tac ~params status =