- 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 status, (_,t), (_,ty) = refine status context t (Some (context,gty)) in
+ to_subst status i (gname,context,t,ty)