S.elements (TI.retrieve_unifiables univ ty)
;;
+let in_universe univ ty =
+ let candidates = get_candidates univ ty in
+ List.fold_left
+ (fun res cand ->
+ match res with
+ | Some found -> Some found
+ | None ->
+ let candty,_ =
+ CicTypeChecker.type_of_aux' [] [] cand CicUniv.oblivion_ugraph in
+ let same ,_ =
+ CicReduction.are_convertible [] candty ty CicUniv.oblivion_ugraph in
+ if same then Some cand else None
+ ) None candidates
+;;
+
let rec unfold context = function
| Cic.Prod(name,s,t) ->
let t' = unfold ((Some (name,Cic.Decl s))::context) t in
(* collapse non-indexable terms, not removing coercions *)
val key: Cic.term -> Cic.term
+val in_universe: universe -> Cic.term -> Cic.term option
+
(* indexes the term and its unfolded both without coercions *)
val index_term_and_unfolded_term:
universe -> Cic.context -> Cic.term -> Cic.term -> universe