+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
+ let status, (_,t), (_,ty) = refine status context t (Some (context,gty)) in
+ to_subst status i (gname,context,t,ty)
+ else
+ let status,(_,ty) = typeof status context t in
+ to_subst status i (gname,context,snd t,ty)
+;;
+
+let instantiate_with_ast status i t =
+ let _,_,metasenv,_,_ = status#obj in
+ let gname, context, gty = List.assoc i metasenv in
+ let ggty = mk_cic_term context gty in
+ let status, (_,t) = disambiguate status context t (Some ggty) in
+ to_subst status i (gname,context,t,gty)
+;;
+
+let mk_meta status ?(attrs=[]) ctx bo_or_ty kind =