+ let (uri,metasenv,subst,bo,ty, attrs), gl = t status in
+ match
+ CicRefine.pack_coercion_obj
+ (Cic.CurrentProof ("",metasenv,Cic.Rel ~-1,ty,[],attrs))
+ with
+ | Cic.CurrentProof (_,metasenv,_,ty,_, attrs) ->
+ (uri,metasenv,subst,bo,ty, attrs), gl
+ | _ -> assert false
+;;