Commit 5bc1e566 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Always notify after adding a transformation, in case no subgoals are created. (Fix for bug #16769)

parent 4b10f0a9
......@@ -1423,7 +1423,7 @@ let remove_file file =
(* transformations *)
(***************************)
let add_transformation ~keygen env_session transfn g goals =
let add_transformation ?(init=notify) ?(notify=notify) ~keygen env_session transfn g goals =
let rtransf = raw_add_transformation ~keygen ~expanded:true g transfn in
let parent = Parent_transf rtransf in
let i = ref 0 in
......@@ -1453,6 +1453,8 @@ let add_transformation ~keygen env_session transfn g goals =
let goals = List.fold_left add_goal [] goals in
rtransf.transf_goals <- List.rev goals;
rtransf.transf_verified <- transf_verified rtransf;
init (Transf rtransf);
check_goal_proved notify g;
rtransf
......
......@@ -396,6 +396,8 @@ val copy_external_proof :
(** {2 Transformation} *)
val add_transformation :
?init:'key notify ->
?notify:'key notify ->
keygen:'key keygen ->
'key env_session ->
string ->
......
......@@ -815,8 +815,7 @@ let transformation_on_goal_aux eS tr keep_dumb_transformation g =
| _ -> true
in
if b then
let ntr = add_transformation ~keygen:O.create eS tr g subgoals in
init_any (Transf ntr);
let ntr = add_transformation ~init:init_any ~notify ~keygen:O.create eS tr g subgoals in
Some ntr
else None
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment