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 =