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