let term_to_refine =
C.MutCase (uri,typeno,outtype,term,patterns)
in
let term_to_refine =
C.MutCase (uri,typeno,outtype,term,patterns)
in
let refined_term,_,metasenv'',_ =
CicRefine.type_of_aux' metasenv' context term_to_refine
CicUniv.empty_ugraph
let refined_term,_,metasenv'',_ =
CicRefine.type_of_aux' metasenv' context term_to_refine
CicUniv.empty_ugraph