+ let rec perforate ctx menv = function
+ | NCic.Appl (NCic.Const (NReference.Ref (u,_))::ty::_)
+ when NUri.string_of_uri u = "cic:/matita/tests/hole.con" ->
+ let menv, ty = perforate ctx menv ty in
+ let a,b,_ = NCicMetaSubst.mk_meta menv ctx (Some ty) in a,b
+ | t ->
+ NCicUntrusted.map_term_fold_a
+ (fun e ctx -> e::ctx) ctx perforate menv t
+ in
+ let ctx, pty = intros ty in
+ let menv, pty = perforate ctx [] pty in
+(*