) 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
in
(* restarts the numbering of named universes (the ones inside the cic) *)
let _ = CicUniv.restart_numbering () in
- (* HACK ORRIBILE: fa in modo che il parser metta degli universi fresh non
- * anonimi *)
- let _ = CicParser3.set_uri uri in
let obj =
try
let time = Unix.gettimeofday() in
- let rc = CicParser.obj_of_xml filename bodyfilename in
+ let rc = CicParser.obj_of_xml uri filename bodyfilename in
total_parsing_time :=
!total_parsing_time +. ((Unix.gettimeofday()) -. time );
rc