+ 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
+ NCicMetaSubst.mk_meta menv ctx ty
+ | 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
+(*