match
CicRefine.pack_coercion_obj
(Cic.CurrentProof ("",metasenv,Cic.Rel ~-1,ty,[],attrs))
with
| Cic.CurrentProof (_,metasenv,_,ty,_, attrs) ->
match
CicRefine.pack_coercion_obj
(Cic.CurrentProof ("",metasenv,Cic.Rel ~-1,ty,[],attrs))
with
| Cic.CurrentProof (_,metasenv,_,ty,_, attrs) ->