first proof reconstruction attempt, still bugged since it

[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 147df78f857f8be9979772a154a3d1c26af10a39..b6b933211b5e0aa7091b43911f4cd123b183e0f1 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -568,7 +568,8 @@ let auto ~params:(l,_) status goal =
         (status, (t,ty) :: l))
       (status,[]) l
   in
-  Paramod.nparamod metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l;      
+  let rdb = status.estatus.NEstatus.rstatus.NRstatus.refiner_status in
+  Paramod.nparamod rdb metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l;      
     status
 ;;