Fix semantics of -force option, now consistent with the doc

doc/manpages.tex

@@ -456,7 +456,7 @@ option \verb|-force| described below.
 \item Option \verb|-s| suppresses the output of the final tree view.
 \item Option \texttt{-I \textsl{<path>}} adds \texttt{\textsl{<path>}} to the loadpath.
 \item Option \verb|-force| enforces saving the session, if all proof
-  attempts replayed correctly, even if some goals are not proved.
+  attempts replayed correctly, even if some goals are not proved. 
 \item Option \texttt{-smoke-detector \{none|top|deep\}} tries to detect
   if the context is self-contradicting.
 \end{itemize}

src/ide/replay.ml

@@ -327,27 +327,27 @@ let add_to_check_no_smoke config found_obs env_session sched =
             report
         in
         if report = [] then begin
-          if !opt_force then
-            printf " %d/%d (replay OK, session going to be saved since -force was given)@." n m
-          else
-            if found_obs then
-              if n=m then
-                printf " %d/%d (replay OK, all proved: obsolete session \
+          if found_obs then
+            if n=m then
+              printf " %d/%d (replay OK, all proved: obsolete session \
 updated)@." n m
+            else
+              if !opt_force then
+                printf " %d/%d (replay OK, but not all proved: session going to be saved since -force was given)@." n m
               else
                 printf " %d/%d (replay OK, but not all proved: obsolete \
 session NOT updated)@." n m
-            else
-              printf " %d/%d@." n m ;
-            if !opt_stats && n<m then print_statistics files;
-            eprintf "Everything replayed OK.@.";
-            if (found_obs && n=m) || !opt_force then
-              begin
-                eprintf "Saving session...@?";
-                S.save_session config session;
-                eprintf " done@."
-              end;
-            exit 0
+          else
+            printf " %d/%d@." n m ;
+          if !opt_stats && n<m then print_statistics files;
+          eprintf "Everything replayed OK.@.";
+          if found_obs && (n=m || !opt_force) then
+            begin
+              eprintf "Saving session...@?";
+              S.save_session config session;
+              eprintf " done@."
+            end;
+          exit 0
         end
         else
           begin