details, related to hi-lite meeting

ROADMAP

@@ -10,6 +10,11 @@
 
 * A true Jessie3 front-end ?
 
+* Why3ML
+** Fast WP a la Leino
+** assert qui ne donne pas une hypothese dans la suite -> "check"
+   also: in a black box
+
 * traceability: Partially done
   (Claude)
   DONE: traceability des hyp comme path dans le prog (depuis

src/ide/replay.ml

@@ -28,7 +28,6 @@ let opt_stats = ref true
 let opt_latex = ref ""
 let opt_latex2 = ref ""
 let opt_longtable = ref false
-let opt_html = ref ""
 let opt_force = ref false
 let opt_smoke = ref Session.SD_None
 
@@ -63,9 +62,6 @@ let spec = Arg.align [
   ("-longtable",
    Arg.Set opt_longtable,
    " produce latex statistics using longtable package") ;
-  ("-html",
-   Arg.Set_string opt_html,
-   " [Dir_output] produce html statistics") ;
 ]
 
 let version_msg = Format.sprintf "Why3 replayer, version %s (build date: %s)"
@@ -460,7 +456,7 @@ let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
 	if Hashtbl.length tr > 0 then
 	  begin
 	    if (Hashtbl.length proofs == 0) then
-	      fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @." (List.length prov);
+	      fprintf fmt "& \\multicolumn{%d}{c|}{}\\\\ @." (List.length prov);
 	    Hashtbl.iter (fun _st tr ->
 		let goals = tr.M.subgoals in
 		let _ = List.fold_left (fun subgoal g ->

src/transform/smoke_detector.ml

@@ -35,6 +35,9 @@ let top = create t_not
 
 let rec neg f = match f.t_node with
   | Tbinop (Timplies,f1,f2) -> t_and f1 (neg f2)
+(* Would show too much smoke ? 
+  | Tbinop (Timplies,f1,f2) -> t_implies f1 (neg f2)
+*)
   | Tquant (Tforall,fq) ->
       let vsl,_trl,f = t_open_quant fq in
       t_forall_close vsl _trl (neg f)