let rec dummies_of_coercions =
function
- | Cic.Appl (c::l) when CoercDb.is_a_coercion' c ->
+ | Cic.Appl (c::l) when CoercDb.is_a_coercion c <> None ->
Cic.Meta (-1,[])
| Cic.Appl l ->
let l' = List.map dummies_of_coercions l in Cic.Appl l'
let remove_uri univ uri =
let term = CicUtil.term_of_uri uri in
- let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.empty_ugraph in
+ let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.oblivion_ugraph in
remove univ [] term ty