+ | Cic.Const _ | Cic.Var _ | Cic.MutInd _ | Cic.MutConstruct _ as t ->
+ (try Constant (CicUtil.uri_of_term t)
+ with Invalid_argument _ -> assert false)
+ | Cic.Appl _ ->
+ assert false (* should not happen *)
+ | Cic.LetIn _ | Cic.Lambda _ | Cic.Prod _ | Cic.Cast _
+ | Cic.MutCase _ | Cic.Fix _ | Cic.CoFix _ ->
+ HLog.debug "FIXME: the trie receives an invalid term";
+ Dead
+ (* assert false universe.ml removes these *)