Commit 69dc560d authored by Claude Marche's avatar Claude Marche

removed a few additional Ocaml 4.00 warnings

parent ca8a20d8
......@@ -806,12 +806,13 @@ $(COQPDEP): $(COQPGENERATED)
byte: src/coq-tactic/.why3-vo-byte
opt: src/coq-tactic/.why3-vo-opt
src/coq-tactic/coqCompat.cmi: BFLAGS+=-rectypes
src/coq-tactic/coqCompat.cmo: BFLAGS+=-rectypes
src/coq-tactic/coqCompat.cmi: BFLAGS+=-rectypes
src/coq-tactic/coqCompat.cmo: BFLAGS+=-rectypes
src/coq-tactic/coqCompat.cmx: OFLAGS+=-rectypes
src/coq-tactic/why3tac.cmo: BFLAGS+=-rectypes -I +camlp5
src/coq-tactic/why3tac.cmx: BFLAGS+=-rectypes -I +camlp5
lib/coq-tactic/why3tac.cma: BFLAGS+=-rectypes -I +camlp5
src/coq-tactic/why3tac.cmi: BFLAGS+=-rectypes -I +camlp5
src/coq-tactic/why3tac.cmo: BFLAGS+=-rectypes -I +camlp5
src/coq-tactic/why3tac.cmx: OFLAGS+=-rectypes -I +camlp5
lib/coq-tactic/why3tac.cma: BFLAGS+=-rectypes -I +camlp5
lib/coq-tactic/why3tac.cmxs: OFLAGS+=-rectypes -I +camlp5
lib/coq-tactic/why3tac.cmxs: src/why3.cmxa $(COQPCMX)
......
......@@ -22,9 +22,7 @@
a graph-based heuristic finds close enough to the goal *)
open Why3
open Util
open Ident
open Ty
open Term
open Decl
open Task
......@@ -37,7 +35,6 @@ module Int_Dft = struct
let default = max_int
end
open Graph
module GP = Graph.Persistent.Digraph.ConcreteLabeled(
struct
type t = lsymbol
......@@ -403,7 +400,7 @@ module Select = struct
in List.fold_left fmla_get_pred acc clause
(** get all sub-formulae *)
let rec get_sub_fmlas fTbl tTbl fmla =
let get_sub_fmlas fTbl tTbl fmla =
let rec gather_sub_fmla fTbl tTbl acc fmla = match fmla.t_node with
| Tapp (_,terms) ->
let acc = List.fold_left (gather_sub_term fTbl tTbl) acc terms in
......
......@@ -425,13 +425,11 @@ let load_env_session ?(includes=[]) session conf_path_opt =
(* session accessor *)
(************************)
(* dead code
let get_session_file file = file.file_parent
(* dead code
let get_session_theory th = get_session_file th.theory_parent
*)
(* dead code
let rec get_session_goal goal =
match goal.goal_parent with
| Parent_transf trans -> get_session_trans trans
......
......@@ -18,7 +18,6 @@
(* *)
(**************************************************************************)
open Format
open Why3
open Ident
......
......@@ -113,7 +113,7 @@ struct
List.fold_left
(fun depth g -> max depth (goal_depth g)) 0 t.S.theory_goals
let rec provers_stats provers theory =
let provers_stats provers theory =
S.theory_iter_proof_attempt (fun a ->
Hashtbl.replace provers a.S.proof_prover a.S.proof_prover) theory
......@@ -166,13 +166,13 @@ let rec num_lines acc tr =
let rec print_transf fmt depth max_depth provers tr =
fprintf fmt "<tr>";
for i=1 to 0 (* depth-1 *) do fprintf fmt "<td></td>" done;
for _i=1 to 0 (* depth-1 *) do fprintf fmt "<td></td>" done;
fprintf fmt "<td bgcolor=\"#%a\" colspan=\"%d\">"
(color_of_status ~dark:false) tr.S.transf_verified
(max_depth - depth + 1);
(* for i=1 to depth-1 do fprintf fmt "&nbsp;&nbsp;&nbsp;&nbsp;" done; *)
fprintf fmt "%s</td>" tr.transf_name ;
for i=1 (* depth *) to (*max_depth - 1 + *) List.length provers do
for _i=1 (* depth *) to (*max_depth - 1 + *) List.length provers do
fprintf fmt "<td bgcolor=\"#E0E0E0\"></td>"
done;
fprintf fmt "</tr>@\n";
......
......@@ -222,7 +222,7 @@ and stats2_of_transf ~nb_proofs tr : (notask goal * notask goal_stat) list =
let print_res fmt (p,t) = fprintf fmt "%a (%.2f)" print_prover p t
let rec print_goal_stats depth (g,l) =
for i=1 to depth do printf " " done;
for _i=1 to depth do printf " " done;
printf "+-- goal %s" g.goal_name.Ident.id_string;
match l with
| No l ->
......@@ -237,7 +237,7 @@ let rec print_goal_stats depth (g,l) =
List.iter (print_transf_stats (depth+1)) l
and print_transf_stats depth (tr,l) =
for i=1 to depth do printf " " done;
for _i=1 to depth do printf " " done;
printf "+-- transformation %s@\n" tr.transf_name;
List.iter (print_goal_stats (depth+1)) l
......
......@@ -20,7 +20,6 @@
open Why3
open Why3session_lib
open Whyconf
open Format
......@@ -118,7 +117,7 @@ let print_head n depth provers fmt =
let print_tabular_head n depth provers fmt =
fprintf fmt "\\begin{tabular}";
fprintf fmt "{| l |";
for i = 0 to (List.length provers) + depth do fprintf fmt "c |" done;
for _i = 0 to (List.length provers) + depth do fprintf fmt "c |" done;
fprintf fmt "}@.";
print_head n depth provers fmt
......@@ -165,11 +164,11 @@ let rec goal_latex_stat fmt prov depth depth_max subgoal g =
if subgoal > 0 then
begin
if(depth < depth_max) then
for i = 1 to depth do
for _i = 1 to depth do
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
done
else
for i = 1 to depth - 1 do
for _i = 1 to depth - 1 do
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
done
end
......@@ -181,7 +180,7 @@ let rec goal_latex_stat fmt prov depth depth_max subgoal g =
else
begin
if subgoal > 0 then
for i = 1 to depth do
for _i = 1 to depth do
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " " done
else
if depth > 0 then
......@@ -197,18 +196,18 @@ let rec goal_latex_stat fmt prov depth depth_max subgoal g =
if depth_max <= 1 then
begin
if depth > 0 then
for i = depth to (depth_max - depth) do
for _i = depth to (depth_max - depth) do
fprintf fmt "& \\explanation{%s}" " " done
else
for i = depth to (depth_max - depth - 1) do
for _i = depth to (depth_max - depth - 1) do
fprintf fmt "& \\explanation{%s}" " " done
end
else
if depth > 0 then
for i = depth to (depth_max - depth - 1) do
for _i = depth to (depth_max - depth - 1) do
fprintf fmt "& \\explanation{%s}" " " done
else
for i = depth to (depth_max - depth - 2) do
for _i = depth to (depth_max - depth - 2) do
fprintf fmt "& \\explanation{%s}" " " done;
print_result_prov proofs prov fmt;
end;
......@@ -230,7 +229,7 @@ let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
fprintf fmt "\\cline{%d-%d} @." 2 column
else
fprintf fmt "\\hline @.";
for i = 1 to depth do fprintf fmt "\\quad" done;
for _i = 1 to depth do fprintf fmt "\\quad" done;
if (depth <= 1) then
fprintf fmt "\\explanation{%s} " (protect (S.goal_expl g))
else
......@@ -285,7 +284,7 @@ let latex_tabular_file n fmt depth provers f =
let latex_longtable n fmt depth name provers t=
fprintf fmt "\\begin{longtable}";
fprintf fmt "{| l |";
for i = 0 to (List.length provers) + depth do fprintf fmt "c |" done;
for _i = 0 to (List.length provers) + depth do fprintf fmt "c |" done;
fprintf fmt "}@.";
(** First head *)
print_head n depth provers fmt;
......
......@@ -72,8 +72,9 @@ let common_options = [
Debug.Opt.desc_debug;
]
(* dead code
let env_spec = common_options
*)
let read_env_spec () =
(** Configuration *)
......
......@@ -20,7 +20,6 @@
open Why3
open Why3session_lib
open Whyconf
open Session
open Format
......
......@@ -55,10 +55,14 @@ let modulename path t =
(** Driver *)
(* dead code
(* (path,id) -> string Hid *)
let stdlib = Hashtbl.create 17
let is_stdlib path id = Hashtbl.mem stdlib (path, id)
*)
(** Printers *)
let ocaml_keywords =
......@@ -77,7 +81,7 @@ let is_ocaml_keyword =
List.iter (fun s -> Hashtbl.add h s ()) ocaml_keywords;
Hashtbl.mem h
let iprinter,aprinter,tprinter,pprinter =
let iprinter,aprinter,_tprinter,_pprinter =
let isanitize = sanitizer char_to_alpha char_to_alnumus in
let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
create_ident_printer ocaml_keywords ~sanitizer:isanitize,
......@@ -88,11 +92,13 @@ let iprinter,aprinter,tprinter,pprinter =
let forget_tvs () =
forget_all aprinter
(* dead code
let forget_all () =
forget_all iprinter;
forget_all aprinter;
forget_all tprinter;
forget_all pprinter
*)
(* info *)
......@@ -494,10 +500,11 @@ and print_tbranch info fmt br =
fprintf fmt "@[<hov 4>| %a ->@ %a@]" (print_pat info) p (print_term info) t;
Svs.iter forget_var p.pat_vars
(* dead code
and print_tl info fmt tl =
if tl = [] then () else fprintf fmt "@ [%a]"
(print_list alt (print_list comma (print_term info))) tl
*)
let print_ls_type info fmt = function
| None -> fprintf fmt "bool"
......
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