Fixed wrong types in proof terms

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index aebcf4614a512866fd68c232e21bb6086d6b9880..0d18b6fabbfd80d1d2e1f34b5858701eddad2364 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -569,8 +569,11 @@ let auto ~params:(l,_) status goal =
       (status,[]) l
   in
   let rdb = status.estatus in
-  Paramod.nparamod rdb metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l;      
-    status
+  let pt, metasenv, subst = 
+    Paramod.nparamod rdb metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
+  in      
+  let status = { status with pstatus = n,h,metasenv,subst,o } in
+  instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
 ;;
 
 let auto_tac ~params status =