[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