Commit c8e489cd authored by MARCHE Claude's avatar MARCHE Claude

resolved ocaml 4.0 warnings

parent 1a1d2bea
......@@ -9,7 +9,6 @@
(* *)
(********************************************************************)
open Stdlib
open Ident
open Ty
open Term
......
......@@ -9,7 +9,6 @@
(* *)
(********************************************************************)
open Stdlib
open Ident
open Ty
open Term
......
......@@ -9,9 +9,7 @@
(* *)
(********************************************************************)
open Format
open Stdlib
open Ident
open Ty
open Term
open Decl
......
......@@ -115,7 +115,9 @@ let rec grep out l = match l with
let debug = Debug.register_info_flag "call_prover"
~desc:"About@ external@ prover@ calls@ and@ results."
(*
type res_waitpid = int * Unix.process_status
*)
type post_prover_call = unit -> prover_result
......
......@@ -13,7 +13,6 @@
open Format
open Pp
open Stdlib
open Ident
open Ty
open Term
......
......@@ -47,7 +47,6 @@ TODO
open Format
open Pp
open Stdlib
open Ident
open Ty
open Term
......
......@@ -147,10 +147,10 @@ and print_fmla info fmt f = match f.t_node with
"smtv1 : you must eliminate match"
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
and print_expr info fmt =
and _print_expr info fmt =
TermTF.t_select (print_term info fmt) (print_fmla info fmt)
and _print_triggers info fmt tl = print_list comma (print_expr info) fmt tl
and _print_triggers info fmt tl = print_list comma (_print_expr info) fmt tl
let _print_logic_binder info fmt v =
......
......@@ -13,7 +13,6 @@
open Format
open Pp
open Stdlib
open Ident
open Ty
open Term
......@@ -37,7 +36,7 @@ let iprinter,aprinter,tprinter,pprinter =
let forget_tvs () =
forget_all aprinter
let forget_all () =
let _forget_all () =
forget_all iprinter;
forget_all aprinter;
forget_all tprinter;
......
......@@ -9,7 +9,6 @@
(* *)
(********************************************************************)
open Stdlib
open Debug
open Stdlib
open Ty
......
......@@ -12,9 +12,7 @@
{
open Lexing
type element =
type element =
{ name : string;
attributes : (string * string) list;
elements : element list;
......
......@@ -9,7 +9,6 @@
(* *)
(********************************************************************)
open Stdlib
open Ident
open Ty
open Term
......
......@@ -9,7 +9,6 @@
(* *)
(********************************************************************)
open Stdlib
open Ident
open Ty
open Term
......
......@@ -9,7 +9,6 @@
(* *)
(********************************************************************)
open Stdlib
open Ty
open Term
open Decl
......
......@@ -9,7 +9,6 @@
(* *)
(********************************************************************)
open Stdlib
open Ident
open Ty
open Term
......
......@@ -9,7 +9,6 @@
(* *)
(********************************************************************)
open Stdlib
open Ident
open Ty
open Term
......
......@@ -63,7 +63,6 @@ let spec =
common_options
open Session
open Stdlib
type context =
(string ->
......
......@@ -9,7 +9,6 @@
(* *)
(********************************************************************)
open Stdlib
open Ident
open Ty
open Term
......
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