From 0c9795cfecb9922e0b3f694a19e0469b01ea98d1 Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Thu, 23 Aug 2012 11:10:30 +0200 Subject: [PATCH] "Clean" was cleaning too much --- CHANGES | 1 + src/session/session_scheduler.ml | 7 +++++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/CHANGES b/CHANGES index 8b3b824a2..7f66cbe93 100644 --- a/CHANGES +++ b/CHANGES @@ -1,6 +1,7 @@ * marks an incompatible change + o [IDE] "Clean" was cleaning too much * no more executable why3ml (why3 now handles WhyML files) o [Provers] support for Z3 4.0 o [Sessions] a small change in the format. Why3 is still able to diff --git a/src/session/session_scheduler.ml b/src/session/session_scheduler.ml index 0d3e18e1d..d5eab84ec 100644 --- a/src/session/session_scheduler.ml +++ b/src/session/session_scheduler.ml @@ -959,8 +959,11 @@ let rec clean = function iter_goal (fun _ -> ()) (fun t -> - if not t.transf_verified then remove_transformation t - else transf_iter clean t) + (* NO !!! + if not t.transf_verified then remove_transformation t + else + *) + transf_iter clean t) (fun m -> if not m.metas_verified then remove_metas m else metas_iter clean m) -- GitLab