Initial implementation of statuses using objects in place of nested records.

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