| C.Cast (v,t) -> C.Cast (aux v, aux t)
| C.Prod (b,s,t) -> C.Prod (b,aux s, aux t)
| C.Lambda (b,s,t) -> C.Lambda (b,aux s, aux t)
- | C.LetIn (b,s,t) -> C.LetIn (b,aux s, aux t)
+ | C.LetIn (b,s,ty,t) -> C.LetIn (b,aux s, aux ty, aux t)
| C.Appl li -> C.Appl (List.map aux li)
| C.MutCase (uri,n1,ty,te,patterns) ->
C.MutCase (uri,n1,aux ty,aux te, List.map aux patterns)
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)
-
-let profiler = (HExtlib.profile "clean_and_fill").HExtlib.profile
+ 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 *)
in
ugraph, list_of_universes, obj
+(*
+let profiler = (HExtlib.profile "clean_and_fill").HExtlib.profile
let clean_and_fill u o g =
profiler (clean_and_fill u o) g
-
+*)