X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnAuto.ml;h=6f49f7d36575b4c9d21cf9e66a768728d1bcda0d;hb=668fb315dc8502dc1b4d336eba19ab9436bf5b7a;hp=65252eaf99e89cdda9d4bf362492dabf30fc7e84;hpb=f1fc99e982ca6c9c939504c4dcf773edf582792a;p=helm.git

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 65252eaf9..6f49f7d36 100644
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -24,6 +24,9 @@ module Ast = CicNotationPt
 
 (* =================================== paramod =========================== *)
 let auto_paramod ~params:(l,_) status goal =
+  let l = match l with
+    | None -> raise (Error (lazy "no proof found",None))
+    | Some l -> l in
   let gty = get_goalty status goal in
   let n,h,metasenv,subst,o = status#obj in
   let status,t = term_of_cic_term status gty (ctx_of gty) in