status#set_obj (name,height,metasenv,subst,obj)
;;
-let instantiate status ?refine:(dorefine=false) i t =
+let instantiate status ?refine:(dorefine=true) i t =
let _,_,metasenv,_,_ = status#obj in
let gname, context, gty = List.assoc i metasenv in
if dorefine then