let t' =
match t with
| None -> None
- | Some t -> Some (fun _ m u -> t, m, u)
+ | Some t -> Some (const_lazy_term t)
in
t',[],Some (Cic.Implicit (Some `Hole))
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
;;