) l
in
C.Meta(i,l')
+ | C.Sort (C.Type u) ->
+ CicUniv.assert_univ u;
+ C.Sort (C.Type (CicUniv.recons_univ u))
| C.Sort _ as t -> t
| C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (restore_in_term te, restore_in_term ty)
in
C.CoFix (i, liftedfl)
in
- function
+ function
C.Constant (name,bo,ty,params,attrs) ->
let bo' =
match bo with
let restore_from_channel = Cache.restore_from_channel;;
let empty = Cache.empty;;
+let total_parsing_time = ref 0.0
+
let get_object_to_add uri =
let filename = Http_getter.getxml' uri in
let bodyfilename =
| None -> ()
end
in
- (* this brakes something :
- * let _ = CicUniv.restart_numbering () in
- *)
+ (* restarts the numbering of named universes (the ones inside the cic) *)
+ let _ = CicUniv.restart_numbering () in
let obj =
try
- CicParser.obj_of_xml filename bodyfilename
+ let time = Unix.gettimeofday() in
+ let rc = CicParser.obj_of_xml uri filename bodyfilename in
+ total_parsing_time :=
+ !total_parsing_time +. ((Unix.gettimeofday()) -. time );
+ rc
with exn ->
cleanup ();
(match exn with