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
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