(* enriched metasenv, new term, its type, metavriable to
* be unified with the old term *)
(NCic.metasenv * NCic.term * NCic.term * NCic.term) list
(* enriched metasenv, new term, its type, metavriable to
* be unified with the old term *)
(NCic.metasenv * NCic.term * NCic.term * NCic.term) list