| NCic.Appl (NCic.Const (NReference.Ref (u,_))::ty::_)
when NUri.string_of_uri u = "cic:/matita/tests/hole.con" ->
let metasenv, ty = perforate ctx metasenv ty in
- let a,b,_ = NCicMetaSubst.mk_meta metasenv ctx (`WithType ty) in a,b
+ let a,_,b,_ =
+ NCicMetaSubst.mk_meta metasenv ctx (`WithType ty) in a,b
| t ->
NCicUntrusted.map_term_fold_a
(fun e ctx -> e::ctx) ctx perforate metasenv t