X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnAuto.ml;h=5c5bb471b7d3c30c1f19ca8712d859eaa56fd098;hb=21ee96d317a4f0e7abfe76f697defe78acc10b94;hp=25f4e0fc70ff52c85f4e49f7630605fcae456bcc;hpb=dce1bca274f93a3bddcc0f6b04cbf126ccff42b0;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)
 ;;