X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnAuto.ml;h=5c5bb471b7d3c30c1f19ca8712d859eaa56fd098;hb=fa6d1f3df955464343b365114be1071fc0b0cd18;hp=25f4e0fc70ff52c85f4e49f7630605fcae456bcc;hpb=0232b651c37511743ce9e99d517a41adac3a7064;p=helm.git

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 25f4e0fc7..5c5bb471b 100644
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -41,7 +41,7 @@ let auto_paramod ~params:(l,_) status goal =
     NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
   with
   | [] -> raise (Error (lazy "no proof found",None))
-  | (pt, metasenv, subst)::_ -> 
+  | (pt, _, metasenv, subst)::_ -> 
       let status = status#set_obj (n,h,metasenv,subst,o) in
       instantiate status goal (mk_cic_term (ctx_of gty) pt)
 ;;