| C.Meta (n,l1) -> C.Meta (n, List.map (HExtlib.map_option aux) l1)
| C.Sort (C.Type i) -> add_result [i];
C.Sort (C.Type (CicUniv.name_universe i uri))
+ | C.Sort (C.CProp i) -> add_result [i];
+ C.Sort (C.CProp (CicUniv.name_universe i uri))
| C.Rel _
| C.Sort _
| C.Implicit _ as x -> x
let o = aux_obj t in
List.flatten !results, o
-let rec list_uniq = function
- | [] -> []
- | h::[] -> [h]
- | h1::h2::tl when CicUniv.eq h1 h2 -> list_uniq (h2 :: tl)
- | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl
-
let list_uniq l =
- list_uniq (List.fast_sort CicUniv.compare l)
+ HExtlib.list_uniq (List.fast_sort CicUniv.compare l)
let clean_and_fill uri obj ugraph =
(* universes of obj fills the universes of the obj with the right uri *)