(CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
else
let new_coercions =
- CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri
+ CicCoercion.close_coercion_graph src_carr tgt_carr uri
baseuri
in
let new_coercions =
let add_obj refinement_toolkit uri obj =
add_single_obj uri obj refinement_toolkit;
let uris = ref [] in
+ let not_debug = not (Helm_registry.get_bool "matita.debug") in
try
begin
match obj with
end;
UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris;
!uris
- with exn ->
- List.iter remove_single_obj !uris;
- raise exn
+ with
+ | exn when not_debug ->
+ List.iter remove_single_obj !uris;
+ raise exn
let remove_obj uri =
let uris =