Commit c3593b6d authored by MARCHE Claude's avatar MARCHE Claude

fix bug when reloading a transformation

parent 67622336
......@@ -873,7 +873,7 @@ and reload_trans ~provers _goal_obsolete goal _ tr =
[] goals
in
mtr.subgoals <- goals;
check_goal_proved goal
check_transf_proved mtr
in
apply_transformation ~callback tr.transf (get_task goal)
......
......@@ -26,7 +26,7 @@ theory TestInt
goal Test5: forall x:int. x <> 0 -> x*x > 0
goal Test6: 2+3 = 6 and (forall x:int. x*x >= 0)
goal Test6: 2+3 = 5 and (forall x:int. x*x >= 0)
goal Test7: 0 = 2 and 2 = 3 and 4 = 5 and 6 = 7
......
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