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'
[head true ty; head true (unfold context ty)]
with ProofEngineTypes.Fail _ -> [head true ty]
-let key term = head false term
+let key term = head false term;;
let index_term_and_unfolded_term univ context t ty =
let key = head true ty in
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