let status, ty = typeof status (ctx_of what) what in
let status, (ref, consno, _, _) = analyse_indty status ty in
let status, what = term_of_cic_term status what (ctx_of gty) in
let t =
NCic.Match (ref,NCic.Implicit `Term, what,
HExtlib.mk_list (NCic.Implicit `Term) consno)
let status, ty = typeof status (ctx_of what) what in
let status, (ref, consno, _, _) = analyse_indty status ty in
let status, what = term_of_cic_term status what (ctx_of gty) in
let t =
NCic.Match (ref,NCic.Implicit `Term, what,
HExtlib.mk_list (NCic.Implicit `Term) consno)