let _,metasenv,_,_ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
let old_context_len = List.length context in
- let termty = CicTypeChecker.type_of_aux' metasenv context term in
-
- let rec make_list termty =
+ let termty,_ =
+ CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ let rec make_list termty =
(* N.B.: altamente inefficente? *)
let rec search_inductive_types urilist termty =
(* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *)
let _,metasenv,_,_ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let old_context_len = List.length context in
- let termty = CicTypeChecker.type_of_aux' metasenv context term' in
+ let termty,_ =
+ CicTypeChecker.type_of_aux' metasenv context term'
+ CicUniv.empty_ugraph in
warn ("elim_clear termty= " ^ CicPp.ppterm termty);
match termty with
C.MutInd (uri,typeno,exp_named_subst)