C.Lambda (name, aux so, aux dest)
| C.LetIn (name,so,dest) ->
C.LetIn (name, aux so, aux dest)
- | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when
+ | Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ] when
CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
let source_carr = CoercGraph.source_of c2 in
let tgt_carr = CoercGraph.target_of c1 in
if CicEnvironment.in_library uri then
raise (AlreadyDefined uri)
else begin
+ (*CicUniv.reset_spent_time ();
+ let before = Unix.gettimeofday () in*)
typecheck_obj uri obj; (* 1 *)
+ (*let after = Unix.gettimeofday () in
+ let univ_time = CicUniv.get_spent_time () in
+ let total_time = after -. before in
+ prerr_endline
+ (Printf.sprintf "QED: %%univ = %2.5f, total = %2.5f, univ = %2.5f, %s\n"
+ (univ_time *. 100. /. total_time) (total_time) (univ_time)
+ (UriManager.name_of_uri uri));*)
let _, ugraph, univlist =
CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in
try
in
(* store that composite_uris are related to uri. the first component is the
* stuff in the DB while the second is stuff for remove_obj *)
+ prerr_endline ("aggiungo: " ^ string_of_bool add_composites ^ UriManager.string_of_uri uri);
+ List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+ composite_uris;
UriManager.UriHashtbl.add coercion_hashtbl uri
(composite_uris,if add_composites then composite_uris else []);
lemmas
let (composites_in_db, composites_in_lib) =
UriManager.UriHashtbl.find coercion_hashtbl uri
in
+ prerr_endline ("removing: " ^UriManager.string_of_uri uri);
+ List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+ composites_in_db;
UriManager.UriHashtbl.remove coercion_hashtbl uri;
CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u);
(* remove from the DB *)
CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
let attrs = [`Class `Projection; `Generated] in
let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
-
add_single_obj ~basedir uri obj;
let composites =
if coercion then